Merge pull request #123 from AeneasVerif/son/clean

Cleanup the code in preparation of the nested loops

21 files changed, 502 insertions, 536 deletions

diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 049d63cb..c9696147 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -36,19 +36,19 @@ Definition array_to_mut_slice_
 (** [arrays::array_len]:
     Source: 'src/arrays.rs', lines 25:0-25:40 *)
 Definition array_len (T : Type) (s : array T 32%usize) : result usize :=
-  s1 <- array_to_slice T 32%usize s; Return (slice_len T s1)
+  s1 <- array_to_slice T 32%usize s; Ok (slice_len T s1)
 .
 
 (** [arrays::shared_array_len]:
     Source: 'src/arrays.rs', lines 29:0-29:48 *)
 Definition shared_array_len (T : Type) (s : array T 32%usize) : result usize :=
-  s1 <- array_to_slice T 32%usize s; Return (slice_len T s1)
+  s1 <- array_to_slice T 32%usize s; Ok (slice_len T s1)
 .
 
 (** [arrays::shared_slice_len]:
     Source: 'src/arrays.rs', lines 33:0-33:44 *)
 Definition shared_slice_len (T : Type) (s : slice T) : result usize :=
-  Return (slice_len T s)
+  Ok (slice_len T s)
 .
 
 (** [arrays::index_array_shared]:
@@ -114,7 +114,7 @@ Definition slice_subslice_mut_
       (core_slice_index_SliceIndexRangeUsizeSliceTInst u32) x
       {| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |};
   let (s, index_mut_back) := p in
-  Return (s, index_mut_back)
+  Ok (s, index_mut_back)
 .
 
 (** [arrays::array_to_slice_shared_]:
@@ -155,7 +155,7 @@ Definition array_subslice_mut_
       (core_slice_index_SliceIndexRangeUsizeSliceTInst u32)) x
       {| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |};
   let (s, index_mut_back) := p in
-  Return (s, index_mut_back)
+  Ok (s, index_mut_back)
 .
 
 (** [arrays::index_slice_0]:
@@ -192,47 +192,46 @@ Definition update_update_array
   let (_, index_mut_back1) := p1 in
   a1 <- index_mut_back1 0%u32;
   _ <- index_mut_back a1;
-  Return tt
+  Ok tt
 .
 
 (** [arrays::array_local_deep_copy]:
     Source: 'src/arrays.rs', lines 118:0-118:43 *)
 Definition array_local_deep_copy (x : array u32 32%usize) : result unit :=
-  Return tt
+  Ok tt
 .
 
 (** [arrays::take_array]:
     Source: 'src/arrays.rs', lines 122:0-122:30 *)
 Definition take_array (a : array u32 2%usize) : result unit :=
-  Return tt.
+  Ok tt.
 
 (** [arrays::take_array_borrow]:
     Source: 'src/arrays.rs', lines 123:0-123:38 *)
 Definition take_array_borrow (a : array u32 2%usize) : result unit :=
-  Return tt
-.
+  Ok tt.
 
 (** [arrays::take_slice]:
     Source: 'src/arrays.rs', lines 124:0-124:28 *)
 Definition take_slice (s : slice u32) : result unit :=
-  Return tt.
+  Ok tt.
 
 (** [arrays::take_mut_slice]:
     Source: 'src/arrays.rs', lines 125:0-125:36 *)
 Definition take_mut_slice (s : slice u32) : result (slice u32) :=
-  Return s.
+  Ok s.
 
 (** [arrays::const_array]:
     Source: 'src/arrays.rs', lines 127:0-127:32 *)
 Definition const_array : result (array u32 2%usize) :=
-  Return (mk_array u32 2%usize [ 0%u32; 0%u32 ])
+  Ok (mk_array u32 2%usize [ 0%u32; 0%u32 ])
 .
 
 (** [arrays::const_slice]:
     Source: 'src/arrays.rs', lines 131:0-131:20 *)
 Definition const_slice : result unit :=
   _ <- array_to_slice u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
-  Return tt
+  Ok tt
 .
 
 (** [arrays::take_all]:
@@ -247,7 +246,7 @@ Definition take_all : result unit :=
   let (s1, to_slice_mut_back) := p in
   s2 <- take_mut_slice s1;
   _ <- to_slice_mut_back s2;
-  Return tt
+  Ok tt
 .
 
 (** [arrays::index_array]:
@@ -272,7 +271,7 @@ Definition index_slice_u32_0 (x : slice u32) : result u32 :=
     Source: 'src/arrays.rs', lines 166:0-166:50 *)
 Definition index_mut_slice_u32_0
   (x : slice u32) : result (u32 * (slice u32)) :=
-  i <- slice_index_usize u32 x 0%usize; Return (i, x)
+  i <- slice_index_usize u32 x 0%usize; Ok (i, x)
 .
 
 (** [arrays::index_all]:
@@ -292,7 +291,7 @@ Definition index_all : result u32 :=
   let (i7, s2) := p1 in
   i8 <- u32_add i6 i7;
   _ <- to_slice_mut_back s2;
-  Return i8
+  Ok i8
 .
 
 (** [arrays::update_array]:
@@ -301,7 +300,7 @@ Definition update_array (x : array u32 2%usize) : result unit :=
   p <- array_index_mut_usize u32 2%usize x 0%usize;
   let (_, index_mut_back) := p in
   _ <- index_mut_back 1%u32;
-  Return tt
+  Ok tt
 .
 
 (** [arrays::update_array_mut_borrow]:
@@ -331,7 +330,7 @@ Definition update_all : result unit :=
   let (s, to_slice_mut_back) := p in
   s1 <- update_mut_slice s;
   _ <- to_slice_mut_back s1;
-  Return tt
+  Ok tt
 .
 
 (** [arrays::range_all]:
@@ -349,7 +348,7 @@ Definition range_all : result unit :=
   let (s, index_mut_back) := p in
   s1 <- update_mut_slice s;
   _ <- index_mut_back s1;
-  Return tt
+  Ok tt
 .
 
 (** [arrays::deref_array_borrow]:
@@ -362,13 +361,13 @@ Definition deref_array_borrow (x : array u32 2%usize) : result u32 :=
     Source: 'src/arrays.rs', lines 219:0-219:54 *)
 Definition deref_array_mut_borrow
   (x : array u32 2%usize) : result (u32 * (array u32 2%usize)) :=
-  i <- array_index_usize u32 2%usize x 0%usize; Return (i, x)
+  i <- array_index_usize u32 2%usize x 0%usize; Ok (i, x)
 .
 
 (** [arrays::take_array_t]:
     Source: 'src/arrays.rs', lines 227:0-227:31 *)
 Definition take_array_t (a : array AB_t 2%usize) : result unit :=
-  Return tt.
+  Ok tt.
 
 (** [arrays::non_copyable_array]:
     Source: 'src/arrays.rs', lines 229:0-229:27 *)
@@ -390,7 +389,7 @@ Fixpoint sum_loop
       sum3 <- u32_add sum1 i2;
       i3 <- usize_add i 1%usize;
       sum_loop n1 s sum3 i3)
-    else Return sum1
+    else Ok sum1
   end
 .
 
@@ -418,7 +417,7 @@ Fixpoint sum2_loop
       sum3 <- u32_add sum1 i4;
       i5 <- usize_add i 1%usize;
       sum2_loop n1 s s2 sum3 i5)
-    else Return sum1
+    else Ok sum1
   end
 .
 
@@ -439,7 +438,7 @@ Definition f0 : result unit :=
   let (_, index_mut_back) := p1 in
   s1 <- index_mut_back 1%u32;
   _ <- to_slice_mut_back s1;
-  Return tt
+  Ok tt
 .
 
 (** [arrays::f1]:
@@ -450,13 +449,13 @@ Definition f1 : result unit :=
       0%usize;
   let (_, index_mut_back) := p in
   _ <- index_mut_back 1%u32;
-  Return tt
+  Ok tt
 .
 
 (** [arrays::f2]:
     Source: 'src/arrays.rs', lines 273:0-273:17 *)
 Definition f2 (i : u32) : result unit :=
-  Return tt.
+  Ok tt.
 
 (** [arrays::f4]:
     Source: 'src/arrays.rs', lines 282:0-282:54 *)
@@ -483,7 +482,7 @@ Definition f3 (n : nat) : result u32 :=
 
 (** [arrays::SZ]
     Source: 'src/arrays.rs', lines 286:0-286:19 *)
-Definition sz_body : result usize := Return 32%usize.
+Definition sz_body : result usize := Ok 32%usize.
 Definition sz : usize := sz_body%global.
 
 (** [arrays::f5]:
@@ -505,7 +504,7 @@ Definition ite : result unit :=
   let (_, s3) := p3 in
   _ <- to_slice_mut_back1 s3;
   _ <- to_slice_mut_back s1;
-  Return tt
+  Ok tt
 .
 
 (** [arrays::zero_slice]: loop 0:
@@ -522,7 +521,7 @@ Fixpoint zero_slice_loop
       i1 <- usize_add i 1%usize;
       a1 <- index_mut_back 0%u8;
       zero_slice_loop n1 a1 i1 len)
-    else Return a
+    else Ok a
   end
 .
 
@@ -541,14 +540,14 @@ Fixpoint iter_mut_slice_loop
   | S n1 =>
     if i s< len
     then (i1 <- usize_add i 1%usize; iter_mut_slice_loop n1 len i1)
-    else Return tt
+    else Ok tt
   end
 .
 
 (** [arrays::iter_mut_slice]:
     Source: 'src/arrays.rs', lines 312:0-312:35 *)
 Definition iter_mut_slice (n : nat) (a : slice u8) : result (slice u8) :=
-  let len := slice_len u8 a in _ <- iter_mut_slice_loop n len 0%usize; Return a
+  let len := slice_len u8 a in _ <- iter_mut_slice_loop n len 0%usize; Ok a
 .
 
 (** [arrays::sum_mut_slice]: loop 0:
@@ -565,7 +564,7 @@ Fixpoint sum_mut_slice_loop
       s1 <- u32_add s i2;
       i3 <- usize_add i 1%usize;
       sum_mut_slice_loop n1 a i3 s1)
-    else Return s
+    else Ok s
   end
 .
 
@@ -573,7 +572,7 @@ Fixpoint sum_mut_slice_loop
     Source: 'src/arrays.rs', lines 320:0-320:42 *)
 Definition sum_mut_slice
   (n : nat) (a : slice u32) : result (u32 * (slice u32)) :=
-  i <- sum_mut_slice_loop n a 0%usize 0%u32; Return (i, a)
+  i <- sum_mut_slice_loop n a 0%usize 0%u32; Ok (i, a)
 .
 
 End Arrays.
diff --git a/tests/coq/arrays/Primitives.v b/tests/coq/arrays/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/arrays/Primitives.v
+++ b/tests/coq/arrays/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
   | OutOfFuel.
 
 Inductive result A :=
-  | Return : A -> result A
+  | Ok : A -> result A
   | Fail_ : error -> result A.
 
-Arguments Return {_} a.
+Arguments Ok {_} a.
 Arguments Fail_ {_}.
 
 Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
   match m with
   | Fail_ e => Fail_ e
-  | Return x => f x
+  | Ok x => f x
   end.
 
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
 Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
 
 Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
 
 (** Monadic assert *)
 Definition massert (b: bool) : result unit :=
-  if b then Return tt else Fail_ Failure.
+  if b then Ok tt else Fail_ Failure.
 
 (** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
-  match a as r return (r = Return x -> A) with
-  | Return a' => fun _  => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+  match a as r return (r = Ok x -> A) with
+  | Ok a' => fun _  => a'
   | Fail_ e   => fun p' =>
       False_rect _ (eq_ind (Fail_ e)
           (fun e : result A =>
           match e with
-          | Return _ => False
+          | Ok _ => False
           | Fail_ e => True
           end)
-        I (Return x) p')
+        I (Ok x) p')
   end p.
 
 Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
 Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
 
 (* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
 
 (*** Misc *)
 
@@ -236,7 +236,7 @@ Import Sumbool.
 
 Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
   match sumbool_of_bool (scalar_in_bounds ty x) with
-  | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+  | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
 
 (*** [alloc] *)
 
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
 Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
-  Return (x, fun x => Return x).
+  Ok (x, fun x => Ok x).
 
 (* Trait instance *)
 Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
   result (T * (T -> result (array T n))) :=
   match array_index_usize T n a i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_update_usize T n a i)
+  | Ok x => Ok (x, array_update_usize T n a i)
   end.
 
 (*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
   result (T * (T -> result (slice T))) :=
   match slice_index_usize T s i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, slice_update_usize T s i)
+  | Ok x => Ok (x, slice_update_usize T s i)
   end.
 
 (*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
   result (slice T * (slice T -> result (array T n))) :=
   match array_to_slice T n a with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_from_slice T n a)
+  | Ok x => Ok (x, array_from_slice T n a)
   end.
 
 Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
 Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
   l <- f (alloc_vec_Vec_to_list v) ;
   match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
-  | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+  | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
 Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
-  alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+  alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
 
 Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
   alloc_vec_Vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
-    then Return (list_update l (usize_to_nat i) x)
+    then Ok (list_update l (usize_to_nat i) x)
     else Fail_ Failure).
 
 (* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
 Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
   result (T * (T -> result (alloc_vec_Vec T))) :=
   match alloc_vec_Vec_index_usize v i with
-  | Return x =>
-    Return (x, alloc_vec_Vec_update_usize v i)
+  | Ok x =>
+    Ok (x, alloc_vec_Vec_update_usize v i)
   | Fail_ e => Fail_ e
   end.
 
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
   x <- inst.(core_slice_index_SliceIndex_get) i s;
   match x with
   | None => Fail_ Failure
-  | Some x => Return x
+  | Some x => Ok x
   end.
 
 (* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 9256b149..80518eab 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -49,13 +49,13 @@ Definition betree_store_leaf_node
 (** [betree_main::betree::fresh_node_id]:
     Source: 'src/betree.rs', lines 55:0-55:48 *)
 Definition betree_fresh_node_id (counter : u64) : result (u64 * u64) :=
-  counter1 <- u64_add counter 1%u64; Return (counter, counter1)
+  counter1 <- u64_add counter 1%u64; Ok (counter, counter1)
 .
 
 (** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]:
     Source: 'src/betree.rs', lines 206:4-206:20 *)
 Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t :=
-  Return {| betree_NodeIdCounter_next_node_id := 0%u64 |}
+  Ok {| betree_NodeIdCounter_next_node_id := 0%u64 |}
 .
 
 (** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]:
@@ -63,7 +63,7 @@ Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t :=
 Definition betree_NodeIdCounter_fresh_id
   (self : betree_NodeIdCounter_t) : result (u64 * betree_NodeIdCounter_t) :=
   i <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64;
-  Return (self.(betree_NodeIdCounter_next_node_id),
+  Ok (self.(betree_NodeIdCounter_next_node_id),
     {| betree_NodeIdCounter_next_node_id := i |})
 .
 
@@ -74,16 +74,16 @@ Definition betree_upsert_update
   match prev with
   | None =>
     match st with
-    | Betree_UpsertFunState_Add v => Return v
-    | Betree_UpsertFunState_Sub _ => Return 0%u64
+    | Betree_UpsertFunState_Add v => Ok v
+    | Betree_UpsertFunState_Sub _ => Ok 0%u64
     end
   | Some prev1 =>
     match st with
     | Betree_UpsertFunState_Add v =>
       margin <- u64_sub core_u64_max prev1;
-      if margin s>= v then u64_add prev1 v else Return core_u64_max
+      if margin s>= v then u64_add prev1 v else Ok core_u64_max
     | Betree_UpsertFunState_Sub v =>
-      if prev1 s>= v then u64_sub prev1 v else Return 0%u64
+      if prev1 s>= v then u64_sub prev1 v else Ok 0%u64
     end
   end
 .
@@ -97,7 +97,7 @@ Fixpoint betree_List_len
   | S n1 =>
     match self with
     | Betree_List_Cons _ tl => i <- betree_List_len T n1 tl; u64_add 1%u64 i
-    | Betree_List_Nil => Return 0%u64
+    | Betree_List_Nil => Ok 0%u64
     end
   end
 .
@@ -112,14 +112,14 @@ Fixpoint betree_List_split_at
   | O => Fail_ OutOfFuel
   | S n2 =>
     if n1 s= 0%u64
-    then Return (Betree_List_Nil, self)
+    then Ok (Betree_List_Nil, self)
     else
       match self with
       | Betree_List_Cons hd tl =>
         i <- u64_sub n1 1%u64;
         p <- betree_List_split_at T n2 tl i;
         let (ls0, ls1) := p in
-        Return (Betree_List_Cons hd ls0, ls1)
+        Ok (Betree_List_Cons hd ls0, ls1)
       | Betree_List_Nil => Fail_ Failure
       end
   end
@@ -130,7 +130,7 @@ Fixpoint betree_List_split_at
 Definition betree_List_push_front
   (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) :=
   let (tl, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
-  Return (Betree_List_Cons x tl)
+  Ok (Betree_List_Cons x tl)
 .
 
 (** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]:
@@ -139,7 +139,7 @@ Definition betree_List_pop_front
   (T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) :=
   let (ls, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
   match ls with
-  | Betree_List_Cons x tl => Return (x, tl)
+  | Betree_List_Cons x tl => Ok (x, tl)
   | Betree_List_Nil => Fail_ Failure
   end
 .
@@ -148,7 +148,7 @@ Definition betree_List_pop_front
     Source: 'src/betree.rs', lines 318:4-318:22 *)
 Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
   match self with
-  | Betree_List_Cons hd _ => Return hd
+  | Betree_List_Cons hd _ => Ok hd
   | Betree_List_Nil => Fail_ Failure
   end
 .
@@ -158,8 +158,8 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
 Definition betree_ListPairU64T_head_has_key
   (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool :=
   match self with
-  | Betree_List_Cons hd _ => let (i, _) := hd in Return (i s= key)
-  | Betree_List_Nil => Return false
+  | Betree_List_Cons hd _ => let (i, _) := hd in Ok (i s= key)
+  | Betree_List_Nil => Ok false
   end
 .
 
@@ -176,12 +176,12 @@ Fixpoint betree_ListPairU64T_partition_at_pivot
     | Betree_List_Cons hd tl =>
       let (i, t) := hd in
       if i s>= pivot
-      then Return (Betree_List_Nil, Betree_List_Cons (i, t) tl)
+      then Ok (Betree_List_Nil, Betree_List_Cons (i, t) tl)
       else (
         p <- betree_ListPairU64T_partition_at_pivot T n1 tl pivot;
         let (ls0, ls1) := p in
-        Return (Betree_List_Cons (i, t) ls0, ls1))
-    | Betree_List_Nil => Return (Betree_List_Nil, Betree_List_Nil)
+        Ok (Betree_List_Cons (i, t) ls0, ls1))
+    | Betree_List_Nil => Ok (Betree_List_Nil, Betree_List_Nil)
     end
   end
 .
@@ -218,7 +218,7 @@ Definition betree_Leaf_split
       betree_Leaf_id := id1;
       betree_Leaf_size := params.(betree_Params_split_size)
     |} in
-  Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2,
+  Ok (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2,
     node_id_cnt2))
 .
 
@@ -236,16 +236,16 @@ Fixpoint betree_Node_lookup_first_message_for_key
     | Betree_List_Cons x next_msgs =>
       let (i, m) := x in
       if i s>= key
-      then Return (Betree_List_Cons (i, m) next_msgs, Return)
+      then Ok (Betree_List_Cons (i, m) next_msgs, Ok)
       else (
         p <- betree_Node_lookup_first_message_for_key n1 key next_msgs;
         let (l, lookup_first_message_for_key_back) := p in
         let back :=
           fun (ret : betree_List_t (u64 * betree_Message_t)) =>
             next_msgs1 <- lookup_first_message_for_key_back ret;
-            Return (Betree_List_Cons (i, m) next_msgs1) in
-        Return (l, back))
-    | Betree_List_Nil => Return (Betree_List_Nil, Return)
+            Ok (Betree_List_Cons (i, m) next_msgs1) in
+        Ok (l, back))
+    | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
     end
   end
 .
@@ -263,12 +263,10 @@ Fixpoint betree_Node_lookup_in_bindings
     | Betree_List_Cons hd tl =>
       let (i, i1) := hd in
       if i s= key
-      then Return (Some i1)
+      then Ok (Some i1)
       else
-        if i s> key
-        then Return None
-        else betree_Node_lookup_in_bindings n1 key tl
-    | Betree_List_Nil => Return None
+        if i s> key then Ok None else betree_Node_lookup_in_bindings n1 key tl
+    | Betree_List_Nil => Ok None
     end
   end
 .
@@ -302,7 +300,7 @@ Fixpoint betree_Node_apply_upserts
       msgs1 <-
         betree_List_push_front (u64 * betree_Message_t) msgs (key,
           Betree_Message_Insert v);
-      Return (st1, (v, msgs1)))
+      Ok (st1, (v, msgs1)))
   end
 .
 
@@ -320,13 +318,13 @@ Fixpoint betree_Internal_lookup_in_children
       p <- betree_Node_lookup n1 self.(betree_Internal_left) key st;
       let (st1, p1) := p in
       let (o, n2) := p1 in
-      Return (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
+      Ok (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
         self.(betree_Internal_pivot) n2 self.(betree_Internal_right))))
     else (
       p <- betree_Node_lookup n1 self.(betree_Internal_right) key st;
       let (st1, p1) := p in
       let (o, n2) := p1 in
-      Return (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
+      Ok (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
         self.(betree_Internal_pivot) self.(betree_Internal_left) n2)))
   end
 
@@ -354,19 +352,19 @@ with betree_Node_lookup
           let (st2, p4) := p3 in
           let (o, node1) := p4 in
           _ <- lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l);
-          Return (st2, (o, Betree_Node_Internal node1)))
+          Ok (st2, (o, Betree_Node_Internal node1)))
         else
           match msg with
           | Betree_Message_Insert v =>
             _ <-
               lookup_first_message_for_key_back (Betree_List_Cons (k,
                 Betree_Message_Insert v) l);
-            Return (st1, (Some v, Betree_Node_Internal node))
+            Ok (st1, (Some v, Betree_Node_Internal node))
           | Betree_Message_Delete =>
             _ <-
               lookup_first_message_for_key_back (Betree_List_Cons (k,
                 Betree_Message_Delete) l);
-            Return (st1, (None, Betree_Node_Internal node))
+            Ok (st1, (None, Betree_Node_Internal node))
           | Betree_Message_Upsert ufs =>
             p3 <- betree_Internal_lookup_in_children n1 node key st1;
             let (st2, p4) := p3 in
@@ -380,20 +378,20 @@ with betree_Node_lookup
             p7 <-
               betree_store_internal_node node1.(betree_Internal_id) msgs1 st3;
             let (st4, _) := p7 in
-            Return (st4, (Some v1, Betree_Node_Internal node1))
+            Ok (st4, (Some v1, Betree_Node_Internal node1))
           end
       | Betree_List_Nil =>
         p2 <- betree_Internal_lookup_in_children n1 node key st1;
         let (st2, p3) := p2 in
         let (o, node1) := p3 in
         _ <- lookup_first_message_for_key_back Betree_List_Nil;
-        Return (st2, (o, Betree_Node_Internal node1))
+        Ok (st2, (o, Betree_Node_Internal node1))
       end
     | Betree_Node_Leaf node =>
       p <- betree_load_leaf_node node.(betree_Leaf_id) st;
       let (st1, bindings) := p in
       o <- betree_Node_lookup_in_bindings n1 key bindings;
-      Return (st1, (o, Betree_Node_Leaf node))
+      Ok (st1, (o, Betree_Node_Leaf node))
     end
   end
 .
@@ -417,8 +415,8 @@ Fixpoint betree_Node_filter_messages_for_key
             m) l);
         let (_, msgs1) := p1 in
         betree_Node_filter_messages_for_key n1 key msgs1)
-      else Return (Betree_List_Cons (k, m) l)
-    | Betree_List_Nil => Return Betree_List_Nil
+      else Ok (Betree_List_Cons (k, m) l)
+    | Betree_List_Nil => Ok Betree_List_Nil
     end
   end
 .
@@ -443,10 +441,10 @@ Fixpoint betree_Node_lookup_first_message_after_key
         let back :=
           fun (ret : betree_List_t (u64 * betree_Message_t)) =>
             next_msgs1 <- lookup_first_message_after_key_back ret;
-            Return (Betree_List_Cons (k, m) next_msgs1) in
-        Return (l, back))
-      else Return (Betree_List_Cons (k, m) next_msgs, Return)
-    | Betree_List_Nil => Return (Betree_List_Nil, Return)
+            Ok (Betree_List_Cons (k, m) next_msgs1) in
+        Ok (l, back))
+      else Ok (Betree_List_Cons (k, m) next_msgs, Ok)
+    | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
     end
   end
 .
@@ -527,7 +525,7 @@ Fixpoint betree_Node_apply_messages_to_internal
       let (i, m) := new_msg in
       msgs1 <- betree_Node_apply_to_internal n1 msgs i m;
       betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl
-    | Betree_List_Nil => Return msgs
+    | Betree_List_Nil => Ok msgs
     end
   end
 .
@@ -546,16 +544,16 @@ Fixpoint betree_Node_lookup_mut_in_bindings
     | Betree_List_Cons hd tl =>
       let (i, i1) := hd in
       if i s>= key
-      then Return (Betree_List_Cons (i, i1) tl, Return)
+      then Ok (Betree_List_Cons (i, i1) tl, Ok)
       else (
         p <- betree_Node_lookup_mut_in_bindings n1 key tl;
         let (l, lookup_mut_in_bindings_back) := p in
         let back :=
           fun (ret : betree_List_t (u64 * u64)) =>
             tl1 <- lookup_mut_in_bindings_back ret;
-            Return (Betree_List_Cons (i, i1) tl1) in
-        Return (l, back))
-    | Betree_List_Nil => Return (Betree_List_Nil, Return)
+            Ok (Betree_List_Cons (i, i1) tl1) in
+        Ok (l, back))
+    | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
     end
   end
 .
@@ -613,7 +611,7 @@ Fixpoint betree_Node_apply_messages_to_leaf
       let (i, m) := new_msg in
       bindings1 <- betree_Node_apply_to_leaf n1 bindings i m;
       betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl
-    | Betree_List_Nil => Return bindings
+    | Betree_List_Nil => Ok bindings
     end
   end
 .
@@ -650,20 +648,20 @@ Fixpoint betree_Internal_flush
             node_id_cnt1 msgs_right st1;
         let (st2, p4) := p3 in
         let (n3, node_id_cnt2) := p4 in
-        Return (st2, (Betree_List_Nil, (mkbetree_Internal_t
+        Ok (st2, (Betree_List_Nil, (mkbetree_Internal_t
           self.(betree_Internal_id) self.(betree_Internal_pivot) n2 n3,
           node_id_cnt2))))
       else
-        Return (st1, (msgs_right, (mkbetree_Internal_t
-          self.(betree_Internal_id) self.(betree_Internal_pivot) n2
-          self.(betree_Internal_right), node_id_cnt1))))
+        Ok (st1, (msgs_right, (mkbetree_Internal_t self.(betree_Internal_id)
+          self.(betree_Internal_pivot) n2 self.(betree_Internal_right),
+          node_id_cnt1))))
     else (
       p1 <-
         betree_Node_apply_messages n1 self.(betree_Internal_right) params
           node_id_cnt msgs_right st;
       let (st1, p2) := p1 in
       let (n2, node_id_cnt1) := p2 in
-      Return (st1, (msgs_left, (mkbetree_Internal_t self.(betree_Internal_id)
+      Ok (st1, (msgs_left, (mkbetree_Internal_t self.(betree_Internal_id)
         self.(betree_Internal_pivot) self.(betree_Internal_left) n2,
         node_id_cnt1))))
   end
@@ -694,12 +692,12 @@ with betree_Node_apply_messages
         p4 <-
           betree_store_internal_node node1.(betree_Internal_id) content2 st2;
         let (st3, _) := p4 in
-        Return (st3, (Betree_Node_Internal node1, node_id_cnt1)))
+        Ok (st3, (Betree_Node_Internal node1, node_id_cnt1)))
       else (
         p1 <-
           betree_store_internal_node node.(betree_Internal_id) content1 st1;
         let (st2, _) := p1 in
-        Return (st2, (Betree_Node_Internal node, node_id_cnt)))
+        Ok (st2, (Betree_Node_Internal node, node_id_cnt)))
     | Betree_Node_Leaf node =>
       p <- betree_load_leaf_node node.(betree_Leaf_id) st;
       let (st1, content) := p in
@@ -713,11 +711,11 @@ with betree_Node_apply_messages
         let (new_node, node_id_cnt1) := p2 in
         p3 <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st2;
         let (st3, _) := p3 in
-        Return (st3, (Betree_Node_Internal new_node, node_id_cnt1)))
+        Ok (st3, (Betree_Node_Internal new_node, node_id_cnt1)))
       else (
         p1 <- betree_store_leaf_node node.(betree_Leaf_id) content1 st1;
         let (st2, _) := p1 in
-        Return (st2, (Betree_Node_Leaf
+        Ok (st2, (Betree_Node_Leaf
           {| betree_Leaf_id := node.(betree_Leaf_id); betree_Leaf_size := len
           |}, node_id_cnt)))
     end
@@ -737,7 +735,7 @@ Definition betree_Node_apply
       (key, new_msg) Betree_List_Nil) st;
   let (st1, p1) := p in
   let (self1, node_id_cnt1) := p1 in
-  Return (st1, (self1, node_id_cnt1))
+  Ok (st1, (self1, node_id_cnt1))
 .
 
 (** [betree_main::betree::{betree_main::betree::BeTree#6}::new]:
@@ -751,7 +749,7 @@ Definition betree_BeTree_new
   let (id, node_id_cnt1) := p in
   p1 <- betree_store_leaf_node id Betree_List_Nil st;
   let (st1, _) := p1 in
-  Return (st1,
+  Ok (st1,
     {|
       betree_BeTree_params :=
         {|
@@ -777,7 +775,7 @@ Definition betree_BeTree_apply
       self.(betree_BeTree_node_id_cnt) key msg st;
   let (st1, p1) := p in
   let (n1, nic) := p1 in
-  Return (st1,
+  Ok (st1,
     {|
       betree_BeTree_params := self.(betree_BeTree_params);
       betree_BeTree_node_id_cnt := nic;
@@ -822,7 +820,7 @@ Definition betree_BeTree_lookup
   p <- betree_Node_lookup n self.(betree_BeTree_root) key st;
   let (st1, p1) := p in
   let (o, n1) := p1 in
-  Return (st1, (o,
+  Ok (st1, (o,
     {|
       betree_BeTree_params := self.(betree_BeTree_params);
       betree_BeTree_node_id_cnt := self.(betree_BeTree_node_id_cnt);
@@ -833,7 +831,7 @@ Definition betree_BeTree_lookup
 (** [betree_main::main]:
     Source: 'src/betree_main.rs', lines 5:0-5:9 *)
 Definition main : result unit :=
-  Return tt.
+  Ok tt.
 
 (** Unit test for [betree_main::main] *)
 Check (main )%return.
diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/betree/Primitives.v
+++ b/tests/coq/betree/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
   | OutOfFuel.
 
 Inductive result A :=
-  | Return : A -> result A
+  | Ok : A -> result A
   | Fail_ : error -> result A.
 
-Arguments Return {_} a.
+Arguments Ok {_} a.
 Arguments Fail_ {_}.
 
 Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
   match m with
   | Fail_ e => Fail_ e
-  | Return x => f x
+  | Ok x => f x
   end.
 
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
 Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
 
 Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
 
 (** Monadic assert *)
 Definition massert (b: bool) : result unit :=
-  if b then Return tt else Fail_ Failure.
+  if b then Ok tt else Fail_ Failure.
 
 (** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
-  match a as r return (r = Return x -> A) with
-  | Return a' => fun _  => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+  match a as r return (r = Ok x -> A) with
+  | Ok a' => fun _  => a'
   | Fail_ e   => fun p' =>
       False_rect _ (eq_ind (Fail_ e)
           (fun e : result A =>
           match e with
-          | Return _ => False
+          | Ok _ => False
           | Fail_ e => True
           end)
-        I (Return x) p')
+        I (Ok x) p')
   end p.
 
 Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
 Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
 
 (* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
 
 (*** Misc *)
 
@@ -236,7 +236,7 @@ Import Sumbool.
 
 Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
   match sumbool_of_bool (scalar_in_bounds ty x) with
-  | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+  | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
 
 (*** [alloc] *)
 
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
 Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
-  Return (x, fun x => Return x).
+  Ok (x, fun x => Ok x).
 
 (* Trait instance *)
 Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
   result (T * (T -> result (array T n))) :=
   match array_index_usize T n a i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_update_usize T n a i)
+  | Ok x => Ok (x, array_update_usize T n a i)
   end.
 
 (*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
   result (T * (T -> result (slice T))) :=
   match slice_index_usize T s i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, slice_update_usize T s i)
+  | Ok x => Ok (x, slice_update_usize T s i)
   end.
 
 (*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
   result (slice T * (slice T -> result (array T n))) :=
   match array_to_slice T n a with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_from_slice T n a)
+  | Ok x => Ok (x, array_from_slice T n a)
   end.
 
 Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
 Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
   l <- f (alloc_vec_Vec_to_list v) ;
   match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
-  | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+  | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
 Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
-  alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+  alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
 
 Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
   alloc_vec_Vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
-    then Return (list_update l (usize_to_nat i) x)
+    then Ok (list_update l (usize_to_nat i) x)
     else Fail_ Failure).
 
 (* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
 Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
   result (T * (T -> result (alloc_vec_Vec T))) :=
   match alloc_vec_Vec_index_usize v i with
-  | Return x =>
-    Return (x, alloc_vec_Vec_update_usize v i)
+  | Ok x =>
+    Ok (x, alloc_vec_Vec_update_usize v i)
   | Fail_ e => Fail_ e
   end.
 
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
   x <- inst.(core_slice_index_SliceIndex_get) i s;
   match x with
   | None => Fail_ Failure
-  | Some x => Return x
+  | Some x => Ok x
   end.
 
 (* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index abec8e88..00b9b889 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -13,8 +13,8 @@ Module Demo.
 Definition choose
   (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
   if b
-  then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
-  else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
+  then let back := fun (ret : T) => Ok (ret, y) in Ok (x, back)
+  else let back := fun (ret : T) => Ok (x, ret) in Ok (y, back)
 .
 
 (** [demo::mul2_add1]:
@@ -37,7 +37,7 @@ Definition incr (x : u32) : result u32 :=
 (** [demo::use_incr]:
     Source: 'src/demo.rs', lines 25:0-25:17 *)
 Definition use_incr : result unit :=
-  x <- incr 0%u32; x1 <- incr x; _ <- incr x1; Return tt
+  x <- incr 0%u32; x1 <- incr x; _ <- incr x1; Ok tt
 .
 
 (** [demo::CList]
@@ -58,9 +58,7 @@ Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T :=
   | S n1 =>
     match l with
     | CList_CCons x tl =>
-      if i s= 0%u32
-      then Return x
-      else (i1 <- u32_sub i 1%u32; list_nth T n1 tl i1)
+      if i s= 0%u32 then Ok x else (i1 <- u32_sub i 1%u32; list_nth T n1 tl i1)
     | CList_CNil => Fail_ Failure
     end
   end
@@ -78,17 +76,15 @@ Fixpoint list_nth_mut
     match l with
     | CList_CCons x tl =>
       if i s= 0%u32
-      then
-        let back := fun (ret : T) => Return (CList_CCons ret tl) in
-        Return (x, back)
+      then let back := fun (ret : T) => Ok (CList_CCons ret tl) in Ok (x, back)
       else (
         i1 <- u32_sub i 1%u32;
         p <- list_nth_mut T n1 tl i1;
         let (t, list_nth_mut_back) := p in
         let back :=
-          fun (ret : T) =>
-            tl1 <- list_nth_mut_back ret; Return (CList_CCons x tl1) in
-        Return (t, back))
+          fun (ret : T) => tl1 <- list_nth_mut_back ret; Ok (CList_CCons x tl1)
+          in
+        Ok (t, back))
     | CList_CNil => Fail_ Failure
     end
   end
@@ -106,16 +102,14 @@ Fixpoint list_nth_mut1_loop
     match l with
     | CList_CCons x tl =>
       if i s= 0%u32
-      then
-        let back := fun (ret : T) => Return (CList_CCons ret tl) in
-        Return (x, back)
+      then let back := fun (ret : T) => Ok (CList_CCons ret tl) in Ok (x, back)
       else (
         i1 <- u32_sub i 1%u32;
         p <- list_nth_mut1_loop T n1 tl i1;
         let (t, back) := p in
-        let back1 :=
-          fun (ret : T) => tl1 <- back ret; Return (CList_CCons x tl1) in
-        Return (t, back1))
+        let back1 := fun (ret : T) => tl1 <- back ret; Ok (CList_CCons x tl1)
+          in
+        Ok (t, back1))
     | CList_CNil => Fail_ Failure
     end
   end
@@ -137,7 +131,7 @@ Fixpoint i32_id (n : nat) (i : i32) : result i32 :=
   | O => Fail_ OutOfFuel
   | S n1 =>
     if i s= 0%i32
-    then Return 0%i32
+    then Ok 0%i32
     else (i1 <- i32_sub i 1%i32; i2 <- i32_id n1 i1; i32_add i2 1%i32)
   end
 .
@@ -157,9 +151,9 @@ Fixpoint list_tail
       let (c, list_tail_back) := p in
       let back :=
         fun (ret : CList_t T) =>
-          tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in
-      Return (c, back)
-    | CList_CNil => Return (CList_CNil, Return)
+          tl1 <- list_tail_back ret; Ok (CList_CCons t tl1) in
+      Ok (c, back)
+    | CList_CNil => Ok (CList_CNil, Ok)
     end
   end
 .
@@ -176,7 +170,7 @@ Arguments Counter_t_incr { _ }.
 (** [demo::{(demo::Counter for usize)}::incr]:
     Source: 'src/demo.rs', lines 102:4-102:31 *)
 Definition counterUsize_incr (self : usize) : result (usize * usize) :=
-  self1 <- usize_add self 1%usize; Return (self, self1)
+  self1 <- usize_add self 1%usize; Ok (self, self1)
 .
 
 (** Trait implementation: [demo::{(demo::Counter for usize)}]
diff --git a/tests/coq/demo/Primitives.v b/tests/coq/demo/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/demo/Primitives.v
+++ b/tests/coq/demo/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
   | OutOfFuel.
 
 Inductive result A :=
-  | Return : A -> result A
+  | Ok : A -> result A
   | Fail_ : error -> result A.
 
-Arguments Return {_} a.
+Arguments Ok {_} a.
 Arguments Fail_ {_}.
 
 Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
   match m with
   | Fail_ e => Fail_ e
-  | Return x => f x
+  | Ok x => f x
   end.
 
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
 Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
 
 Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
 
 (** Monadic assert *)
 Definition massert (b: bool) : result unit :=
-  if b then Return tt else Fail_ Failure.
+  if b then Ok tt else Fail_ Failure.
 
 (** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
-  match a as r return (r = Return x -> A) with
-  | Return a' => fun _  => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+  match a as r return (r = Ok x -> A) with
+  | Ok a' => fun _  => a'
   | Fail_ e   => fun p' =>
       False_rect _ (eq_ind (Fail_ e)
           (fun e : result A =>
           match e with
-          | Return _ => False
+          | Ok _ => False
           | Fail_ e => True
           end)
-        I (Return x) p')
+        I (Ok x) p')
   end p.
 
 Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
 Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
 
 (* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
 
 (*** Misc *)
 
@@ -236,7 +236,7 @@ Import Sumbool.
 
 Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
   match sumbool_of_bool (scalar_in_bounds ty x) with
-  | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+  | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
 
 (*** [alloc] *)
 
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
 Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
-  Return (x, fun x => Return x).
+  Ok (x, fun x => Ok x).
 
 (* Trait instance *)
 Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
   result (T * (T -> result (array T n))) :=
   match array_index_usize T n a i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_update_usize T n a i)
+  | Ok x => Ok (x, array_update_usize T n a i)
   end.
 
 (*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
   result (T * (T -> result (slice T))) :=
   match slice_index_usize T s i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, slice_update_usize T s i)
+  | Ok x => Ok (x, slice_update_usize T s i)
   end.
 
 (*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
   result (slice T * (slice T -> result (array T n))) :=
   match array_to_slice T n a with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_from_slice T n a)
+  | Ok x => Ok (x, array_from_slice T n a)
   end.
 
 Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
 Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
   l <- f (alloc_vec_Vec_to_list v) ;
   match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
-  | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+  | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
 Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
-  alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+  alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
 
 Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
   alloc_vec_Vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
-    then Return (list_update l (usize_to_nat i) x)
+    then Ok (list_update l (usize_to_nat i) x)
     else Fail_ Failure).
 
 (* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
 Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
   result (T * (T -> result (alloc_vec_Vec T))) :=
   match alloc_vec_Vec_index_usize v i with
-  | Return x =>
-    Return (x, alloc_vec_Vec_update_usize v i)
+  | Ok x =>
+    Ok (x, alloc_vec_Vec_update_usize v i)
   | Fail_ e => Fail_ e
   end.
 
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
   x <- inst.(core_slice_index_SliceIndex_get) i s;
   match x with
   | None => Fail_ Failure
-  | Some x => Return x
+  | Some x => Ok x
   end.
 
 (* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index c0cde78d..ebb7897d 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -13,7 +13,7 @@ Module Hashmap_Funs.
 (** [hashmap::hash_key]:
     Source: 'src/hashmap.rs', lines 27:0-27:32 *)
 Definition hash_key (k : usize) : result usize :=
-  Return k.
+  Ok k.
 
 (** [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
     Source: 'src/hashmap.rs', lines 50:4-56:5 *)
@@ -29,7 +29,7 @@ Fixpoint hashMap_allocate_slots_loop
       slots1 <- alloc_vec_Vec_push (List_t T) slots List_Nil;
       n3 <- usize_sub n1 1%usize;
       hashMap_allocate_slots_loop T n2 slots1 n3)
-    else Return slots
+    else Ok slots
   end
 .
 
@@ -52,7 +52,7 @@ Definition hashMap_new_with_capacity
   slots <- hashMap_allocate_slots T n (alloc_vec_Vec_new (List_t T)) capacity;
   i <- usize_mul capacity max_load_dividend;
   i1 <- usize_div i max_load_divisor;
-  Return
+  Ok
     {|
       hashMap_num_entries := 0%usize;
       hashMap_max_load_factor := (max_load_dividend, max_load_divisor);
@@ -86,7 +86,7 @@ Fixpoint hashMap_clear_loop
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back List_Nil;
       hashMap_clear_loop T n1 slots1 i2)
-    else Return slots
+    else Ok slots
   end
 .
 
@@ -95,7 +95,7 @@ Fixpoint hashMap_clear_loop
 Definition hashMap_clear
   (T : Type) (n : nat) (self : HashMap_t T) : result (HashMap_t T) :=
   hm <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize;
-  Return
+  Ok
     {|
       hashMap_num_entries := 0%usize;
       hashMap_max_load_factor := self.(hashMap_max_load_factor);
@@ -107,7 +107,7 @@ Definition hashMap_clear
 (** [hashmap::{hashmap::HashMap<T>}::len]:
     Source: 'src/hashmap.rs', lines 90:4-90:30 *)
 Definition hashMap_len (T : Type) (self : HashMap_t T) : result usize :=
-  Return self.(hashMap_num_entries)
+  Ok self.(hashMap_num_entries)
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
@@ -122,12 +122,12 @@ Fixpoint hashMap_insert_in_list_loop
     match ls with
     | List_Cons ckey cvalue tl =>
       if ckey s= key
-      then Return (false, List_Cons ckey value tl)
+      then Ok (false, List_Cons ckey value tl)
       else (
         p <- hashMap_insert_in_list_loop T n1 key value tl;
         let (b, tl1) := p in
-        Return (b, List_Cons ckey cvalue tl1))
-    | List_Nil => Return (true, List_Cons key value List_Nil)
+        Ok (b, List_Cons ckey cvalue tl1))
+    | List_Nil => Ok (true, List_Cons key value List_Nil)
     end
   end
 .
@@ -161,7 +161,7 @@ Definition hashMap_insert_no_resize
   then (
     i1 <- usize_add self.(hashMap_num_entries) 1%usize;
     v <- index_mut_back l1;
-    Return
+    Ok
       {|
         hashMap_num_entries := i1;
         hashMap_max_load_factor := self.(hashMap_max_load_factor);
@@ -170,7 +170,7 @@ Definition hashMap_insert_no_resize
       |})
   else (
     v <- index_mut_back l1;
-    Return
+    Ok
       {|
         hashMap_num_entries := self.(hashMap_num_entries);
         hashMap_max_load_factor := self.(hashMap_max_load_factor);
@@ -192,7 +192,7 @@ Fixpoint hashMap_move_elements_from_list_loop
     | List_Cons k v tl =>
       ntable1 <- hashMap_insert_no_resize T n1 ntable k v;
       hashMap_move_elements_from_list_loop T n1 ntable1 tl
-    | List_Nil => Return ntable
+    | List_Nil => Ok ntable
     end
   end
 .
@@ -228,7 +228,7 @@ Fixpoint hashMap_move_elements_loop
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back l1;
       hashMap_move_elements_loop T n1 ntable1 slots1 i2)
-    else Return (ntable, slots)
+    else Ok (ntable, slots)
   end
 .
 
@@ -257,7 +257,7 @@ Definition hashMap_try_resize
     ntable <- hashMap_new_with_capacity T n i3 i i1;
     p <- hashMap_move_elements T n ntable self.(hashMap_slots) 0%usize;
     let (ntable1, _) := p in
-    Return
+    Ok
       {|
         hashMap_num_entries := self.(hashMap_num_entries);
         hashMap_max_load_factor := (i, i1);
@@ -265,7 +265,7 @@ Definition hashMap_try_resize
         hashMap_slots := ntable1.(hashMap_slots)
       |})
   else
-    Return
+    Ok
       {|
         hashMap_num_entries := self.(hashMap_num_entries);
         hashMap_max_load_factor := (i, i1);
@@ -284,7 +284,7 @@ Definition hashMap_insert
   i <- hashMap_len T self1;
   if i s> self1.(hashMap_max_load)
   then hashMap_try_resize T n self1
-  else Return self1
+  else Ok self1
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
@@ -297,9 +297,9 @@ Fixpoint hashMap_contains_key_in_list_loop
     match ls with
     | List_Cons ckey _ tl =>
       if ckey s= key
-      then Return true
+      then Ok true
       else hashMap_contains_key_in_list_loop T n1 key tl
-    | List_Nil => Return false
+    | List_Nil => Ok false
     end
   end
 .
@@ -334,9 +334,7 @@ Fixpoint hashMap_get_in_list_loop
   | S n1 =>
     match ls with
     | List_Cons ckey cvalue tl =>
-      if ckey s= key
-      then Return cvalue
-      else hashMap_get_in_list_loop T n1 key tl
+      if ckey s= key then Ok cvalue else hashMap_get_in_list_loop T n1 key tl
     | List_Nil => Fail_ Failure
     end
   end
@@ -376,15 +374,14 @@ Fixpoint hashMap_get_mut_in_list_loop
     | List_Cons ckey cvalue tl =>
       if ckey s= key
       then
-        let back := fun (ret : T) => Return (List_Cons ckey ret tl) in
-        Return (cvalue, back)
+        let back := fun (ret : T) => Ok (List_Cons ckey ret tl) in
+        Ok (cvalue, back)
       else (
         p <- hashMap_get_mut_in_list_loop T n1 tl key;
         let (t, back) := p in
         let back1 :=
-          fun (ret : T) => tl1 <- back ret; Return (List_Cons ckey cvalue tl1)
-          in
-        Return (t, back1))
+          fun (ret : T) => tl1 <- back ret; Ok (List_Cons ckey cvalue tl1) in
+        Ok (t, back1))
     | List_Nil => Fail_ Failure
     end
   end
@@ -419,14 +416,14 @@ Definition hashMap_get_mut
     fun (ret : T) =>
       l1 <- get_mut_in_list_back ret;
       v <- index_mut_back l1;
-      Return
+      Ok
         {|
           hashMap_num_entries := self.(hashMap_num_entries);
           hashMap_max_load_factor := self.(hashMap_max_load_factor);
           hashMap_max_load := self.(hashMap_max_load);
           hashMap_slots := v
         |} in
-  Return (t, back)
+  Ok (t, back)
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
@@ -445,14 +442,14 @@ Fixpoint hashMap_remove_from_list_loop
         let (mv_ls, _) :=
           core_mem_replace (List_t T) (List_Cons ckey t tl) List_Nil in
         match mv_ls with
-        | List_Cons _ cvalue tl1 => Return (Some cvalue, tl1)
+        | List_Cons _ cvalue tl1 => Ok (Some cvalue, tl1)
         | List_Nil => Fail_ Failure
         end
       else (
         p <- hashMap_remove_from_list_loop T n1 key tl;
         let (o, tl1) := p in
-        Return (o, List_Cons ckey t tl1))
-    | List_Nil => Return (None, List_Nil)
+        Ok (o, List_Cons ckey t tl1))
+    | List_Nil => Ok (None, List_Nil)
     end
   end
 .
@@ -485,7 +482,7 @@ Definition hashMap_remove
   match x with
   | None =>
     v <- index_mut_back l1;
-    Return (None,
+    Ok (None,
       {|
         hashMap_num_entries := self.(hashMap_num_entries);
         hashMap_max_load_factor := self.(hashMap_max_load_factor);
@@ -495,7 +492,7 @@ Definition hashMap_remove
   | Some x1 =>
     i1 <- usize_sub self.(hashMap_num_entries) 1%usize;
     v <- index_mut_back l1;
-    Return (Some x1,
+    Ok (Some x1,
       {|
         hashMap_num_entries := i1;
         hashMap_max_load_factor := self.(hashMap_max_load_factor);
@@ -541,7 +538,7 @@ Definition test1 (n : nat) : result unit :=
             then Fail_ Failure
             else (
               i4 <- hashMap_get u64 n hm6 1056%usize;
-              if negb (i4 s= 256%u64) then Fail_ Failure else Return tt)))
+              if negb (i4 s= 256%u64) then Fail_ Failure else Ok tt)))
       end))
 .
 
diff --git a/tests/coq/hashmap/Primitives.v b/tests/coq/hashmap/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/hashmap/Primitives.v
+++ b/tests/coq/hashmap/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
   | OutOfFuel.
 
 Inductive result A :=
-  | Return : A -> result A
+  | Ok : A -> result A
   | Fail_ : error -> result A.
 
-Arguments Return {_} a.
+Arguments Ok {_} a.
 Arguments Fail_ {_}.
 
 Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
   match m with
   | Fail_ e => Fail_ e
-  | Return x => f x
+  | Ok x => f x
   end.
 
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
 Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
 
 Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
 
 (** Monadic assert *)
 Definition massert (b: bool) : result unit :=
-  if b then Return tt else Fail_ Failure.
+  if b then Ok tt else Fail_ Failure.
 
 (** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
-  match a as r return (r = Return x -> A) with
-  | Return a' => fun _  => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+  match a as r return (r = Ok x -> A) with
+  | Ok a' => fun _  => a'
   | Fail_ e   => fun p' =>
       False_rect _ (eq_ind (Fail_ e)
           (fun e : result A =>
           match e with
-          | Return _ => False
+          | Ok _ => False
           | Fail_ e => True
           end)
-        I (Return x) p')
+        I (Ok x) p')
   end p.
 
 Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
 Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
 
 (* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
 
 (*** Misc *)
 
@@ -236,7 +236,7 @@ Import Sumbool.
 
 Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
   match sumbool_of_bool (scalar_in_bounds ty x) with
-  | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+  | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
 
 (*** [alloc] *)
 
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
 Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
-  Return (x, fun x => Return x).
+  Ok (x, fun x => Ok x).
 
 (* Trait instance *)
 Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
   result (T * (T -> result (array T n))) :=
   match array_index_usize T n a i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_update_usize T n a i)
+  | Ok x => Ok (x, array_update_usize T n a i)
   end.
 
 (*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
   result (T * (T -> result (slice T))) :=
   match slice_index_usize T s i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, slice_update_usize T s i)
+  | Ok x => Ok (x, slice_update_usize T s i)
   end.
 
 (*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
   result (slice T * (slice T -> result (array T n))) :=
   match array_to_slice T n a with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_from_slice T n a)
+  | Ok x => Ok (x, array_from_slice T n a)
   end.
 
 Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
 Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
   l <- f (alloc_vec_Vec_to_list v) ;
   match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
-  | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+  | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
 Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
-  alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+  alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
 
 Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
   alloc_vec_Vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
-    then Return (list_update l (usize_to_nat i) x)
+    then Ok (list_update l (usize_to_nat i) x)
     else Fail_ Failure).
 
 (* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
 Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
   result (T * (T -> result (alloc_vec_Vec T))) :=
   match alloc_vec_Vec_index_usize v i with
-  | Return x =>
-    Return (x, alloc_vec_Vec_update_usize v i)
+  | Ok x =>
+    Ok (x, alloc_vec_Vec_update_usize v i)
   | Fail_ e => Fail_ e
   end.
 
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
   x <- inst.(core_slice_index_SliceIndex_get) i s;
   match x with
   | None => Fail_ Failure
-  | Some x => Return x
+  | Some x => Ok x
   end.
 
 (* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 8e299800..79da6e80 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -15,7 +15,7 @@ Module HashmapMain_Funs.
 (** [hashmap_main::hashmap::hash_key]:
     Source: 'src/hashmap.rs', lines 27:0-27:32 *)
 Definition hashmap_hash_key (k : usize) : result usize :=
-  Return k.
+  Ok k.
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: loop 0:
     Source: 'src/hashmap.rs', lines 50:4-56:5 *)
@@ -32,7 +32,7 @@ Fixpoint hashmap_HashMap_allocate_slots_loop
       slots1 <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil;
       n3 <- usize_sub n1 1%usize;
       hashmap_HashMap_allocate_slots_loop T n2 slots1 n3)
-    else Return slots
+    else Ok slots
   end
 .
 
@@ -58,7 +58,7 @@ Definition hashmap_HashMap_new_with_capacity
       capacity;
   i <- usize_mul capacity max_load_dividend;
   i1 <- usize_div i max_load_divisor;
-  Return
+  Ok
     {|
       hashmap_HashMap_num_entries := 0%usize;
       hashmap_HashMap_max_load_factor := (max_load_dividend, max_load_divisor);
@@ -94,7 +94,7 @@ Fixpoint hashmap_HashMap_clear_loop
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back Hashmap_List_Nil;
       hashmap_HashMap_clear_loop T n1 slots1 i2)
-    else Return slots
+    else Ok slots
   end
 .
 
@@ -105,7 +105,7 @@ Definition hashmap_HashMap_clear
   result (hashmap_HashMap_t T)
   :=
   hm <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize;
-  Return
+  Ok
     {|
       hashmap_HashMap_num_entries := 0%usize;
       hashmap_HashMap_max_load_factor := self.(hashmap_HashMap_max_load_factor);
@@ -118,7 +118,7 @@ Definition hashmap_HashMap_clear
     Source: 'src/hashmap.rs', lines 90:4-90:30 *)
 Definition hashmap_HashMap_len
   (T : Type) (self : hashmap_HashMap_t T) : result usize :=
-  Return self.(hashmap_HashMap_num_entries)
+  Ok self.(hashmap_HashMap_num_entries)
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: loop 0:
@@ -133,13 +133,13 @@ Fixpoint hashmap_HashMap_insert_in_list_loop
     match ls with
     | Hashmap_List_Cons ckey cvalue tl =>
       if ckey s= key
-      then Return (false, Hashmap_List_Cons ckey value tl)
+      then Ok (false, Hashmap_List_Cons ckey value tl)
       else (
         p <- hashmap_HashMap_insert_in_list_loop T n1 key value tl;
         let (b, tl1) := p in
-        Return (b, Hashmap_List_Cons ckey cvalue tl1))
+        Ok (b, Hashmap_List_Cons ckey cvalue tl1))
     | Hashmap_List_Nil =>
-      Return (true, Hashmap_List_Cons key value Hashmap_List_Nil)
+      Ok (true, Hashmap_List_Cons key value Hashmap_List_Nil)
     end
   end
 .
@@ -173,7 +173,7 @@ Definition hashmap_HashMap_insert_no_resize
   then (
     i1 <- usize_add self.(hashmap_HashMap_num_entries) 1%usize;
     v <- index_mut_back l1;
-    Return
+    Ok
       {|
         hashmap_HashMap_num_entries := i1;
         hashmap_HashMap_max_load_factor :=
@@ -183,7 +183,7 @@ Definition hashmap_HashMap_insert_no_resize
       |})
   else (
     v <- index_mut_back l1;
-    Return
+    Ok
       {|
         hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
         hashmap_HashMap_max_load_factor :=
@@ -206,7 +206,7 @@ Fixpoint hashmap_HashMap_move_elements_from_list_loop
     | Hashmap_List_Cons k v tl =>
       ntable1 <- hashmap_HashMap_insert_no_resize T n1 ntable k v;
       hashmap_HashMap_move_elements_from_list_loop T n1 ntable1 tl
-    | Hashmap_List_Nil => Return ntable
+    | Hashmap_List_Nil => Ok ntable
     end
   end
 .
@@ -243,7 +243,7 @@ Fixpoint hashmap_HashMap_move_elements_loop
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back l1;
       hashmap_HashMap_move_elements_loop T n1 ntable1 slots1 i2)
-    else Return (ntable, slots)
+    else Ok (ntable, slots)
   end
 .
 
@@ -277,7 +277,7 @@ Definition hashmap_HashMap_try_resize
       hashmap_HashMap_move_elements T n ntable self.(hashmap_HashMap_slots)
         0%usize;
     let (ntable1, _) := p in
-    Return
+    Ok
       {|
         hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
         hashmap_HashMap_max_load_factor := (i, i1);
@@ -285,7 +285,7 @@ Definition hashmap_HashMap_try_resize
         hashmap_HashMap_slots := ntable1.(hashmap_HashMap_slots)
       |})
   else
-    Return
+    Ok
       {|
         hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
         hashmap_HashMap_max_load_factor := (i, i1);
@@ -304,7 +304,7 @@ Definition hashmap_HashMap_insert
   i <- hashmap_HashMap_len T self1;
   if i s> self1.(hashmap_HashMap_max_load)
   then hashmap_HashMap_try_resize T n self1
-  else Return self1
+  else Ok self1
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
@@ -317,9 +317,9 @@ Fixpoint hashmap_HashMap_contains_key_in_list_loop
     match ls with
     | Hashmap_List_Cons ckey _ tl =>
       if ckey s= key
-      then Return true
+      then Ok true
       else hashmap_HashMap_contains_key_in_list_loop T n1 key tl
-    | Hashmap_List_Nil => Return false
+    | Hashmap_List_Nil => Ok false
     end
   end
 .
@@ -357,7 +357,7 @@ Fixpoint hashmap_HashMap_get_in_list_loop
     match ls with
     | Hashmap_List_Cons ckey cvalue tl =>
       if ckey s= key
-      then Return cvalue
+      then Ok cvalue
       else hashmap_HashMap_get_in_list_loop T n1 key tl
     | Hashmap_List_Nil => Fail_ Failure
     end
@@ -398,15 +398,15 @@ Fixpoint hashmap_HashMap_get_mut_in_list_loop
     | Hashmap_List_Cons ckey cvalue tl =>
       if ckey s= key
       then
-        let back := fun (ret : T) => Return (Hashmap_List_Cons ckey ret tl) in
-        Return (cvalue, back)
+        let back := fun (ret : T) => Ok (Hashmap_List_Cons ckey ret tl) in
+        Ok (cvalue, back)
       else (
         p <- hashmap_HashMap_get_mut_in_list_loop T n1 tl key;
         let (t, back) := p in
         let back1 :=
           fun (ret : T) =>
-            tl1 <- back ret; Return (Hashmap_List_Cons ckey cvalue tl1) in
-        Return (t, back1))
+            tl1 <- back ret; Ok (Hashmap_List_Cons ckey cvalue tl1) in
+        Ok (t, back1))
     | Hashmap_List_Nil => Fail_ Failure
     end
   end
@@ -441,7 +441,7 @@ Definition hashmap_HashMap_get_mut
     fun (ret : T) =>
       l1 <- get_mut_in_list_back ret;
       v <- index_mut_back l1;
-      Return
+      Ok
         {|
           hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
           hashmap_HashMap_max_load_factor :=
@@ -449,7 +449,7 @@ Definition hashmap_HashMap_get_mut
           hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load);
           hashmap_HashMap_slots := v
         |} in
-  Return (t, back)
+  Ok (t, back)
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
@@ -469,14 +469,14 @@ Fixpoint hashmap_HashMap_remove_from_list_loop
           core_mem_replace (hashmap_List_t T) (Hashmap_List_Cons ckey t tl)
             Hashmap_List_Nil in
         match mv_ls with
-        | Hashmap_List_Cons _ cvalue tl1 => Return (Some cvalue, tl1)
+        | Hashmap_List_Cons _ cvalue tl1 => Ok (Some cvalue, tl1)
         | Hashmap_List_Nil => Fail_ Failure
         end
       else (
         p <- hashmap_HashMap_remove_from_list_loop T n1 key tl;
         let (o, tl1) := p in
-        Return (o, Hashmap_List_Cons ckey t tl1))
-    | Hashmap_List_Nil => Return (None, Hashmap_List_Nil)
+        Ok (o, Hashmap_List_Cons ckey t tl1))
+    | Hashmap_List_Nil => Ok (None, Hashmap_List_Nil)
     end
   end
 .
@@ -509,7 +509,7 @@ Definition hashmap_HashMap_remove
   match x with
   | None =>
     v <- index_mut_back l1;
-    Return (None,
+    Ok (None,
       {|
         hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
         hashmap_HashMap_max_load_factor :=
@@ -520,7 +520,7 @@ Definition hashmap_HashMap_remove
   | Some x1 =>
     i1 <- usize_sub self.(hashmap_HashMap_num_entries) 1%usize;
     v <- index_mut_back l1;
-    Return (Some x1,
+    Ok (Some x1,
       {|
         hashmap_HashMap_num_entries := i1;
         hashmap_HashMap_max_load_factor :=
@@ -567,7 +567,7 @@ Definition hashmap_test1 (n : nat) : result unit :=
             then Fail_ Failure
             else (
               i4 <- hashmap_HashMap_get u64 n hm6 1056%usize;
-              if negb (i4 s= 256%u64) then Fail_ Failure else Return tt)))
+              if negb (i4 s= 256%u64) then Fail_ Failure else Ok tt)))
       end))
 .
 
@@ -584,6 +584,6 @@ Definition insert_on_disk
 (** [hashmap_main::main]:
     Source: 'src/hashmap_main.rs', lines 16:0-16:13 *)
 Definition main : result unit :=
-  Return tt.
+  Ok tt.
 
 End HashmapMain_Funs.
diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/hashmap_on_disk/Primitives.v
+++ b/tests/coq/hashmap_on_disk/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
   | OutOfFuel.
 
 Inductive result A :=
-  | Return : A -> result A
+  | Ok : A -> result A
   | Fail_ : error -> result A.
 
-Arguments Return {_} a.
+Arguments Ok {_} a.
 Arguments Fail_ {_}.
 
 Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
   match m with
   | Fail_ e => Fail_ e
-  | Return x => f x
+  | Ok x => f x
   end.
 
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
 Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
 
 Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
 
 (** Monadic assert *)
 Definition massert (b: bool) : result unit :=
-  if b then Return tt else Fail_ Failure.
+  if b then Ok tt else Fail_ Failure.
 
 (** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
-  match a as r return (r = Return x -> A) with
-  | Return a' => fun _  => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+  match a as r return (r = Ok x -> A) with
+  | Ok a' => fun _  => a'
   | Fail_ e   => fun p' =>
       False_rect _ (eq_ind (Fail_ e)
           (fun e : result A =>
           match e with
-          | Return _ => False
+          | Ok _ => False
           | Fail_ e => True
           end)
-        I (Return x) p')
+        I (Ok x) p')
   end p.
 
 Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
 Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
 
 (* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
 
 (*** Misc *)
 
@@ -236,7 +236,7 @@ Import Sumbool.
 
 Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
   match sumbool_of_bool (scalar_in_bounds ty x) with
-  | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+  | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
 
 (*** [alloc] *)
 
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
 Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
-  Return (x, fun x => Return x).
+  Ok (x, fun x => Ok x).
 
 (* Trait instance *)
 Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
   result (T * (T -> result (array T n))) :=
   match array_index_usize T n a i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_update_usize T n a i)
+  | Ok x => Ok (x, array_update_usize T n a i)
   end.
 
 (*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
   result (T * (T -> result (slice T))) :=
   match slice_index_usize T s i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, slice_update_usize T s i)
+  | Ok x => Ok (x, slice_update_usize T s i)
   end.
 
 (*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
   result (slice T * (slice T -> result (array T n))) :=
   match array_to_slice T n a with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_from_slice T n a)
+  | Ok x => Ok (x, array_from_slice T n a)
   end.
 
 Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
 Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
   l <- f (alloc_vec_Vec_to_list v) ;
   match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
-  | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+  | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
 Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
-  alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+  alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
 
 Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
   alloc_vec_Vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
-    then Return (list_update l (usize_to_nat i) x)
+    then Ok (list_update l (usize_to_nat i) x)
     else Fail_ Failure).
 
 (* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
 Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
   result (T * (T -> result (alloc_vec_Vec T))) :=
   match alloc_vec_Vec_index_usize v i with
-  | Return x =>
-    Return (x, alloc_vec_Vec_update_usize v i)
+  | Ok x =>
+    Ok (x, alloc_vec_Vec_update_usize v i)
   | Fail_ e => Fail_ e
   end.
 
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
   x <- inst.(core_slice_index_SliceIndex_get) i s;
   match x with
   | None => Fail_ Failure
-  | Some x => Return x
+  | Some x => Ok x
   end.
 
 (* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/misc/Bitwise.v b/tests/coq/misc/Bitwise.v
index b04c95f2..b2339c58 100644
--- a/tests/coq/misc/Bitwise.v
+++ b/tests/coq/misc/Bitwise.v
@@ -23,16 +23,16 @@ Definition shift_i32 (a : i32) : result i32 :=
 (** [bitwise::xor_u32]:
     Source: 'src/bitwise.rs', lines 17:0-17:37 *)
 Definition xor_u32 (a : u32) (b : u32) : result u32 :=
-  Return (u32_xor a b).
+  Ok (u32_xor a b).
 
 (** [bitwise::or_u32]:
     Source: 'src/bitwise.rs', lines 21:0-21:36 *)
 Definition or_u32 (a : u32) (b : u32) : result u32 :=
-  Return (u32_or a b).
+  Ok (u32_or a b).
 
 (** [bitwise::and_u32]:
     Source: 'src/bitwise.rs', lines 25:0-25:37 *)
 Definition and_u32 (a : u32) (b : u32) : result u32 :=
-  Return (u32_and a b).
+  Ok (u32_and a b).
 
 End Bitwise.
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index fcafed53..71185975 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -10,17 +10,17 @@ Module Constants.
 
 (** [constants::X0]
     Source: 'src/constants.rs', lines 5:0-5:17 *)
-Definition x0_body : result u32 := Return 0%u32.
+Definition x0_body : result u32 := Ok 0%u32.
 Definition x0 : u32 := x0_body%global.
 
 (** [constants::X1]
     Source: 'src/constants.rs', lines 7:0-7:17 *)
-Definition x1_body : result u32 := Return core_u32_max.
+Definition x1_body : result u32 := Ok core_u32_max.
 Definition x1 : u32 := x1_body%global.
 
 (** [constants::X2]
     Source: 'src/constants.rs', lines 10:0-10:17 *)
-Definition x2_body : result u32 := Return 3%u32.
+Definition x2_body : result u32 := Ok 3%u32.
 Definition x2 : u32 := x2_body%global.
 
 (** [constants::incr]:
@@ -36,8 +36,7 @@ Definition x3 : u32 := x3_body%global.
 (** [constants::mk_pair0]:
     Source: 'src/constants.rs', lines 23:0-23:51 *)
 Definition mk_pair0 (x : u32) (y1 : u32) : result (u32 * u32) :=
-  Return (x, y1)
-.
+  Ok (x, y1).
 
 (** [constants::Pair]
     Source: 'src/constants.rs', lines 36:0-36:23 *)
@@ -50,7 +49,7 @@ Arguments pair_y { _ _ }.
 (** [constants::mk_pair1]:
     Source: 'src/constants.rs', lines 27:0-27:55 *)
 Definition mk_pair1 (x : u32) (y1 : u32) : result (Pair_t u32 u32) :=
-  Return {| pair_x := x; pair_y := y1 |}
+  Ok {| pair_x := x; pair_y := y1 |}
 .
 
 (** [constants::P0]
@@ -65,13 +64,13 @@ Definition p1 : Pair_t u32 u32 := p1_body%global.
 
 (** [constants::P2]
     Source: 'src/constants.rs', lines 33:0-33:24 *)
-Definition p2_body : result (u32 * u32) := Return (0%u32, 1%u32).
+Definition p2_body : result (u32 * u32) := Ok (0%u32, 1%u32).
 Definition p2 : (u32 * u32) := p2_body%global.
 
 (** [constants::P3]
     Source: 'src/constants.rs', lines 34:0-34:28 *)
 Definition p3_body : result (Pair_t u32 u32) :=
-  Return {| pair_x := 0%u32; pair_y := 1%u32 |}
+  Ok {| pair_x := 0%u32; pair_y := 1%u32 |}
 .
 Definition p3 : Pair_t u32 u32 := p3_body%global.
 
@@ -85,7 +84,7 @@ Arguments wrap_value { _ }.
 (** [constants::{constants::Wrap<T>}::new]:
     Source: 'src/constants.rs', lines 54:4-54:41 *)
 Definition wrap_new (T : Type) (value : T) : result (Wrap_t T) :=
-  Return {| wrap_value := value |}
+  Ok {| wrap_value := value |}
 .
 
 (** [constants::Y]
@@ -96,7 +95,7 @@ Definition y : Wrap_t i32 := y_body%global.
 (** [constants::unwrap_y]:
     Source: 'src/constants.rs', lines 43:0-43:30 *)
 Definition unwrap_y : result i32 :=
-  Return y.(wrap_value).
+  Ok y.(wrap_value).
 
 (** [constants::YVAL]
     Source: 'src/constants.rs', lines 47:0-47:19 *)
@@ -105,13 +104,13 @@ Definition yval : i32 := yval_body%global.
 
 (** [constants::get_z1::Z1]
     Source: 'src/constants.rs', lines 62:4-62:17 *)
-Definition get_z1_z1_body : result i32 := Return 3%i32.
+Definition get_z1_z1_body : result i32 := Ok 3%i32.
 Definition get_z1_z1 : i32 := get_z1_z1_body%global.
 
 (** [constants::get_z1]:
     Source: 'src/constants.rs', lines 61:0-61:28 *)
 Definition get_z1 : result i32 :=
-  Return get_z1_z1.
+  Ok get_z1_z1.
 
 (** [constants::add]:
     Source: 'src/constants.rs', lines 66:0-66:39 *)
@@ -120,12 +119,12 @@ Definition add (a : i32) (b : i32) : result i32 :=
 
 (** [constants::Q1]
     Source: 'src/constants.rs', lines 74:0-74:17 *)
-Definition q1_body : result i32 := Return 5%i32.
+Definition q1_body : result i32 := Ok 5%i32.
 Definition q1 : i32 := q1_body%global.
 
 (** [constants::Q2]
     Source: 'src/constants.rs', lines 75:0-75:17 *)
-Definition q2_body : result i32 := Return q1.
+Definition q2_body : result i32 := Ok q1.
 Definition q2 : i32 := q2_body%global.
 
 (** [constants::Q3]
@@ -140,7 +139,7 @@ Definition get_z2 : result i32 :=
 
 (** [constants::S1]
     Source: 'src/constants.rs', lines 80:0-80:18 *)
-Definition s1_body : result u32 := Return 6%u32.
+Definition s1_body : result u32 := Ok 6%u32.
 Definition s1 : u32 := s1_body%global.
 
 (** [constants::S2]
@@ -150,7 +149,7 @@ Definition s2 : u32 := s2_body%global.
 
 (** [constants::S3]
     Source: 'src/constants.rs', lines 82:0-82:29 *)
-Definition s3_body : result (Pair_t u32 u32) := Return p3.
+Definition s3_body : result (Pair_t u32 u32) := Ok p3.
 Definition s3 : Pair_t u32 u32 := s3_body%global.
 
 (** [constants::S4]
@@ -167,12 +166,12 @@ Arguments v_x { _ _ }.
 
 (** [constants::{constants::V<T, N>#1}::LEN]
     Source: 'src/constants.rs', lines 91:4-91:24 *)
-Definition v_len_body (T : Type) (N : usize) : result usize := Return N.
+Definition v_len_body (T : Type) (N : usize) : result usize := Ok N.
 Definition v_len (T : Type) (N : usize) : usize := (v_len_body T N)%global.
 
 (** [constants::use_v]:
     Source: 'src/constants.rs', lines 94:0-94:42 *)
 Definition use_v (T : Type) (N : usize) : result usize :=
-  Return (v_len T N).
+  Ok (v_len T N).
 
 End Constants.
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index a6832854..41d4a7bd 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -31,7 +31,7 @@ Definition test_new_non_zero_u32
 (** [external::test_vec]:
     Source: 'src/external.rs', lines 17:0-17:17 *)
 Definition test_vec : result unit :=
-  _ <- alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0%u32; Return tt
+  _ <- alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0%u32; Ok tt
 .
 
 (** Unit test for [external::test_vec] *)
@@ -46,8 +46,8 @@ Definition custom_swap
   p <- core_mem_swap T x y st;
   let (st1, p1) := p in
   let (x1, y1) := p1 in
-  let back := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
-  Return (st1, (x1, back))
+  let back := fun (ret : T) (st2 : state) => Ok (st2, (ret, y1)) in
+  Ok (st1, (x1, back))
 .
 
 (** [external::test_custom_swap]:
@@ -60,7 +60,7 @@ Definition test_custom_swap
   p2 <- custom_swap_back 1%u32 st1;
   let (_, p3) := p2 in
   let (x1, y1) := p3 in
-  Return (st1, (x1, y1))
+  Ok (st1, (x1, y1))
 .
 
 (** [external::test_swap_non_zero]:
@@ -69,7 +69,7 @@ Definition test_swap_non_zero (x : u32) (st : state) : result (state * u32) :=
   p <- swap u32 x 0%u32 st;
   let (st1, p1) := p in
   let (x1, _) := p1 in
-  if x1 s= 0%u32 then Fail_ Failure else Return (st1, x1)
+  if x1 s= 0%u32 then Fail_ Failure else Ok (st1, x1)
 .
 
 End External_Funs.
diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v
index e9655f57..130b48a2 100644
--- a/tests/coq/misc/External_FunsExternal.v
+++ b/tests/coq/misc/External_FunsExternal.v
@@ -13,7 +13,7 @@ Module External_FunsExternal.
 (** [core::mem::swap]:
     Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
 Definition core_mem_swap (T : Type) (x : T) (y : T) (s : state) :=
-  Return (s, (y, x))
+  Ok (s, (y, x))
 .
 
 (** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index ae529cf8..f396f16f 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -83,7 +83,7 @@ Fixpoint sum_array_loop
       s1 <- u32_add s i1;
       i2 <- usize_add i 1%usize;
       sum_array_loop N n1 a i2 s1)
-    else Return s
+    else Ok s
   end
 .
 
@@ -110,7 +110,7 @@ Fixpoint clear_loop
       i2 <- usize_add i 1%usize;
       v1 <- index_mut_back 0%u32;
       clear_loop n1 v1 i2)
-    else Return v
+    else Ok v
   end
 .
 
@@ -138,8 +138,8 @@ Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool :=
   | O => Fail_ OutOfFuel
   | S n1 =>
     match ls with
-    | List_Cons y tl => if y s= x then Return true else list_mem_loop n1 x tl
-    | List_Nil => Return false
+    | List_Cons y tl => if y s= x then Ok true else list_mem_loop n1 x tl
+    | List_Nil => Ok false
     end
   end
 .
@@ -162,16 +162,13 @@ Fixpoint list_nth_mut_loop_loop
     match ls with
     | List_Cons x tl =>
       if i s= 0%u32
-      then
-        let back := fun (ret : T) => Return (List_Cons ret tl) in
-        Return (x, back)
+      then let back := fun (ret : T) => Ok (List_Cons ret tl) in Ok (x, back)
       else (
         i1 <- u32_sub i 1%u32;
         p <- list_nth_mut_loop_loop T n1 tl i1;
         let (t, back) := p in
-        let back1 := fun (ret : T) => tl1 <- back ret; Return (List_Cons x tl1)
-          in
-        Return (t, back1))
+        let back1 := fun (ret : T) => tl1 <- back ret; Ok (List_Cons x tl1) in
+        Ok (t, back1))
     | List_Nil => Fail_ Failure
     end
   end
@@ -196,7 +193,7 @@ Fixpoint list_nth_shared_loop_loop
     match ls with
     | List_Cons x tl =>
       if i s= 0%u32
-      then Return x
+      then Ok x
       else (i1 <- u32_sub i 1%u32; list_nth_shared_loop_loop T n1 tl i1)
     | List_Nil => Fail_ Failure
     end
@@ -223,14 +220,13 @@ Fixpoint get_elem_mut_loop
     | List_Cons y tl =>
       if y s= x
       then
-        let back := fun (ret : usize) => Return (List_Cons ret tl) in
-        Return (y, back)
+        let back := fun (ret : usize) => Ok (List_Cons ret tl) in Ok (y, back)
       else (
         p <- get_elem_mut_loop n1 x tl;
         let (i, back) := p in
-        let back1 :=
-          fun (ret : usize) => tl1 <- back ret; Return (List_Cons y tl1) in
-        Return (i, back1))
+        let back1 := fun (ret : usize) => tl1 <- back ret; Ok (List_Cons y tl1)
+          in
+        Ok (i, back1))
     | List_Nil => Fail_ Failure
     end
   end
@@ -249,7 +245,7 @@ Definition get_elem_mut
   p1 <- get_elem_mut_loop n x ls;
   let (i, back) := p1 in
   let back1 := fun (ret : usize) => l <- back ret; index_mut_back l in
-  Return (i, back1)
+  Ok (i, back1)
 .
 
 (** [loops::get_elem_shared]: loop 0:
@@ -260,8 +256,7 @@ Fixpoint get_elem_shared_loop
   | O => Fail_ OutOfFuel
   | S n1 =>
     match ls with
-    | List_Cons y tl =>
-      if y s= x then Return y else get_elem_shared_loop n1 x tl
+    | List_Cons y tl => if y s= x then Ok y else get_elem_shared_loop n1 x tl
     | List_Nil => Fail_ Failure
     end
   end
@@ -285,14 +280,13 @@ Definition id_mut
   (T : Type) (ls : List_t T) :
   result ((List_t T) * (List_t T -> result (List_t T)))
   :=
-  Return (ls, Return)
+  Ok (ls, Ok)
 .
 
 (** [loops::id_shared]:
     Source: 'src/loops.rs', lines 149:0-149:45 *)
 Definition id_shared (T : Type) (ls : List_t T) : result (List_t T) :=
-  Return ls
-.
+  Ok ls.
 
 (** [loops::list_nth_mut_loop_with_id]: loop 0:
     Source: 'src/loops.rs', lines 154:0-165:1 *)
@@ -306,16 +300,13 @@ Fixpoint list_nth_mut_loop_with_id_loop
     match ls with
     | List_Cons x tl =>
       if i s= 0%u32
-      then
-        let back := fun (ret : T) => Return (List_Cons ret tl) in
-        Return (x, back)
+      then let back := fun (ret : T) => Ok (List_Cons ret tl) in Ok (x, back)
       else (
         i1 <- u32_sub i 1%u32;
         p <- list_nth_mut_loop_with_id_loop T n1 i1 tl;
         let (t, back) := p in
-        let back1 := fun (ret : T) => tl1 <- back ret; Return (List_Cons x tl1)
-          in
-        Return (t, back1))
+        let back1 := fun (ret : T) => tl1 <- back ret; Ok (List_Cons x tl1) in
+        Ok (t, back1))
     | List_Nil => Fail_ Failure
     end
   end
@@ -332,7 +323,7 @@ Definition list_nth_mut_loop_with_id
   p1 <- list_nth_mut_loop_with_id_loop T n i ls1;
   let (t, back) := p1 in
   let back1 := fun (ret : T) => l <- back ret; id_mut_back l in
-  Return (t, back1)
+  Ok (t, back1)
 .
 
 (** [loops::list_nth_shared_loop_with_id]: loop 0:
@@ -345,7 +336,7 @@ Fixpoint list_nth_shared_loop_with_id_loop
     match ls with
     | List_Cons x tl =>
       if i s= 0%u32
-      then Return x
+      then Ok x
       else (
         i1 <- u32_sub i 1%u32; list_nth_shared_loop_with_id_loop T n1 i1 tl)
     | List_Nil => Fail_ Failure
@@ -375,18 +366,18 @@ Fixpoint list_nth_mut_loop_pair_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back'a := fun (ret : T) => Return (List_Cons ret tl0) in
-          let back'b := fun (ret : T) => Return (List_Cons ret tl1) in
-          Return ((x0, x1), back'a, back'b)
+          let back'a := fun (ret : T) => Ok (List_Cons ret tl0) in
+          let back'b := fun (ret : T) => Ok (List_Cons ret tl1) in
+          Ok ((x0, x1), back'a, back'b)
         else (
           i1 <- u32_sub i 1%u32;
           t <- list_nth_mut_loop_pair_loop T n1 tl0 tl1 i1;
           let '(p, back'a, back'b) := t in
           let back'a1 :=
-            fun (ret : T) => tl01 <- back'a ret; Return (List_Cons x0 tl01) in
+            fun (ret : T) => tl01 <- back'a ret; Ok (List_Cons x0 tl01) in
           let back'b1 :=
-            fun (ret : T) => tl11 <- back'b ret; Return (List_Cons x1 tl11) in
-          Return (p, back'a1, back'b1))
+            fun (ret : T) => tl11 <- back'b ret; Ok (List_Cons x1 tl11) in
+          Ok (p, back'a1, back'b1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -417,7 +408,7 @@ Fixpoint list_nth_shared_loop_pair_loop
       match ls1 with
       | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (x0, x1)
+        then Ok (x0, x1)
         else (
           i1 <- u32_sub i 1%u32; list_nth_shared_loop_pair_loop T n1 tl0 tl1 i1)
       | List_Nil => Fail_ Failure
@@ -453,9 +444,8 @@ Fixpoint list_nth_mut_loop_pair_merge_loop
         then
           let back :=
             fun (ret : (T * T)) =>
-              let (t, t1) := ret in Return (List_Cons t tl0, List_Cons t1 tl1)
-            in
-          Return ((x0, x1), back)
+              let (t, t1) := ret in Ok (List_Cons t tl0, List_Cons t1 tl1) in
+          Ok ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
@@ -464,8 +454,8 @@ Fixpoint list_nth_mut_loop_pair_merge_loop
             fun (ret : (T * T)) =>
               p2 <- back ret;
               let (tl01, tl11) := p2 in
-              Return (List_Cons x0 tl01, List_Cons x1 tl11) in
-          Return (p1, back1))
+              Ok (List_Cons x0 tl01, List_Cons x1 tl11) in
+          Ok (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -496,7 +486,7 @@ Fixpoint list_nth_shared_loop_pair_merge_loop
       match ls1 with
       | List_Cons x1 tl1 =>
         if i s= 0%u32
-        then Return (x0, x1)
+        then Ok (x0, x1)
         else (
           i1 <- u32_sub i 1%u32;
           list_nth_shared_loop_pair_merge_loop T n1 tl0 tl1 i1)
@@ -531,15 +521,15 @@ Fixpoint list_nth_mut_shared_loop_pair_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back := fun (ret : T) => Return (List_Cons ret tl0) in
-          Return ((x0, x1), back)
+          let back := fun (ret : T) => Ok (List_Cons ret tl0) in
+          Ok ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_mut_shared_loop_pair_loop T n1 tl0 tl1 i1;
           let (p1, back) := p in
           let back1 :=
-            fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
-          Return (p1, back1))
+            fun (ret : T) => tl01 <- back ret; Ok (List_Cons x0 tl01) in
+          Ok (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -571,15 +561,15 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back := fun (ret : T) => Return (List_Cons ret tl0) in
-          Return ((x0, x1), back)
+          let back := fun (ret : T) => Ok (List_Cons ret tl0) in
+          Ok ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_mut_shared_loop_pair_merge_loop T n1 tl0 tl1 i1;
           let (p1, back) := p in
           let back1 :=
-            fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
-          Return (p1, back1))
+            fun (ret : T) => tl01 <- back ret; Ok (List_Cons x0 tl01) in
+          Ok (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -611,15 +601,15 @@ Fixpoint list_nth_shared_mut_loop_pair_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back := fun (ret : T) => Return (List_Cons ret tl1) in
-          Return ((x0, x1), back)
+          let back := fun (ret : T) => Ok (List_Cons ret tl1) in
+          Ok ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_shared_mut_loop_pair_loop T n1 tl0 tl1 i1;
           let (p1, back) := p in
           let back1 :=
-            fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
-          Return (p1, back1))
+            fun (ret : T) => tl11 <- back ret; Ok (List_Cons x1 tl11) in
+          Ok (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -651,15 +641,15 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back := fun (ret : T) => Return (List_Cons ret tl1) in
-          Return ((x0, x1), back)
+          let back := fun (ret : T) => Ok (List_Cons ret tl1) in
+          Ok ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_shared_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
           let (p1, back) := p in
           let back1 :=
-            fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
-          Return (p1, back1))
+            fun (ret : T) => tl11 <- back ret; Ok (List_Cons x1 tl11) in
+          Ok (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -684,7 +674,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   | S n1 =>
     if i s> 0%u32
     then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1)
-    else Return tt
+    else Ok tt
   end
 .
 
@@ -692,7 +682,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
     Source: 'src/loops.rs', lines 345:0-345:56 *)
 Definition ignore_input_mut_borrow
   (n : nat) (_a : u32) (i : u32) : result u32 :=
-  _ <- ignore_input_mut_borrow_loop n i; Return _a
+  _ <- ignore_input_mut_borrow_loop n i; Ok _a
 .
 
 (** [loops::incr_ignore_input_mut_borrow]: loop 0:
@@ -703,7 +693,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   | S n1 =>
     if i s> 0%u32
     then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1)
-    else Return tt
+    else Ok tt
   end
 .
 
@@ -711,7 +701,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
     Source: 'src/loops.rs', lines 353:0-353:60 *)
 Definition incr_ignore_input_mut_borrow
   (n : nat) (a : u32) (i : u32) : result u32 :=
-  a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Return a1
+  a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Ok a1
 .
 
 (** [loops::ignore_input_shared_borrow]: loop 0:
@@ -722,7 +712,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
   | S n1 =>
     if i s> 0%u32
     then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1)
-    else Return tt
+    else Ok tt
   end
 .
 
@@ -730,7 +720,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
     Source: 'src/loops.rs', lines 362:0-362:59 *)
 Definition ignore_input_shared_borrow
   (n : nat) (_a : u32) (i : u32) : result u32 :=
-  _ <- ignore_input_shared_borrow_loop n i; Return _a
+  _ <- ignore_input_shared_borrow_loop n i; Ok _a
 .
 
 End Loops.
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index d4035104..ecdfb281 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -170,12 +170,12 @@ Definition cast_bool_to_i32 (x : bool) : result i32 :=
 (** [no_nested_borrows::cast_bool_to_bool]:
     Source: 'src/no_nested_borrows.rs', lines 137:0-137:41 *)
 Definition cast_bool_to_bool (x : bool) : result bool :=
-  Return x.
+  Ok x.
 
 (** [no_nested_borrows::test2]:
     Source: 'src/no_nested_borrows.rs', lines 142:0-142:14 *)
 Definition test2 : result unit :=
-  _ <- u32_add 23%u32 44%u32; Return tt.
+  _ <- u32_add 23%u32 44%u32; Ok tt.
 
 (** Unit test for [no_nested_borrows::test2] *)
 Check (test2 )%return.
@@ -183,7 +183,7 @@ Check (test2 )%return.
 (** [no_nested_borrows::get_max]:
     Source: 'src/no_nested_borrows.rs', lines 154:0-154:37 *)
 Definition get_max (x : u32) (y : u32) : result u32 :=
-  if x s>= y then Return x else Return y
+  if x s>= y then Ok x else Ok y
 .
 
 (** [no_nested_borrows::test3]:
@@ -192,7 +192,7 @@ Definition test3 : result unit :=
   x <- get_max 4%u32 3%u32;
   y <- get_max 10%u32 11%u32;
   z <- u32_add x y;
-  if negb (z s= 15%u32) then Fail_ Failure else Return tt
+  if negb (z s= 15%u32) then Fail_ Failure else Ok tt
 .
 
 (** Unit test for [no_nested_borrows::test3] *)
@@ -201,7 +201,7 @@ Check (test3 )%return.
 (** [no_nested_borrows::test_neg1]:
     Source: 'src/no_nested_borrows.rs', lines 169:0-169:18 *)
 Definition test_neg1 : result unit :=
-  y <- i32_neg 3%i32; if negb (y s= (-3)%i32) then Fail_ Failure else Return tt
+  y <- i32_neg 3%i32; if negb (y s= (-3)%i32) then Fail_ Failure else Ok tt
 .
 
 (** Unit test for [no_nested_borrows::test_neg1] *)
@@ -210,7 +210,7 @@ Check (test_neg1 )%return.
 (** [no_nested_borrows::refs_test1]:
     Source: 'src/no_nested_borrows.rs', lines 176:0-176:19 *)
 Definition refs_test1 : result unit :=
-  if negb (1%i32 s= 1%i32) then Fail_ Failure else Return tt
+  if negb (1%i32 s= 1%i32) then Fail_ Failure else Ok tt
 .
 
 (** Unit test for [no_nested_borrows::refs_test1] *)
@@ -227,7 +227,7 @@ Definition refs_test2 : result unit :=
     else
       if negb (2%i32 s= 2%i32)
       then Fail_ Failure
-      else if negb (2%i32 s= 2%i32) then Fail_ Failure else Return tt
+      else if negb (2%i32 s= 2%i32) then Fail_ Failure else Ok tt
 .
 
 (** Unit test for [no_nested_borrows::refs_test2] *)
@@ -236,7 +236,7 @@ Check (refs_test2 )%return.
 (** [no_nested_borrows::test_list1]:
     Source: 'src/no_nested_borrows.rs', lines 203:0-203:19 *)
 Definition test_list1 : result unit :=
-  Return tt.
+  Ok tt.
 
 (** Unit test for [no_nested_borrows::test_list1] *)
 Check (test_list1 )%return.
@@ -248,7 +248,7 @@ Definition test_box1 : result unit :=
   let (_, deref_mut_back) := p in
   b <- deref_mut_back 1%i32;
   x <- alloc_boxed_Box_deref i32 b;
-  if negb (x s= 1%i32) then Fail_ Failure else Return tt
+  if negb (x s= 1%i32) then Fail_ Failure else Ok tt
 .
 
 (** Unit test for [no_nested_borrows::test_box1] *)
@@ -257,24 +257,24 @@ Check (test_box1 )%return.
 (** [no_nested_borrows::copy_int]:
     Source: 'src/no_nested_borrows.rs', lines 218:0-218:30 *)
 Definition copy_int (x : i32) : result i32 :=
-  Return x.
+  Ok x.
 
 (** [no_nested_borrows::test_unreachable]:
     Source: 'src/no_nested_borrows.rs', lines 224:0-224:32 *)
 Definition test_unreachable (b : bool) : result unit :=
-  if b then Fail_ Failure else Return tt
+  if b then Fail_ Failure else Ok tt
 .
 
 (** [no_nested_borrows::test_panic]:
     Source: 'src/no_nested_borrows.rs', lines 232:0-232:26 *)
 Definition test_panic (b : bool) : result unit :=
-  if b then Fail_ Failure else Return tt
+  if b then Fail_ Failure else Ok tt
 .
 
 (** [no_nested_borrows::test_copy_int]:
     Source: 'src/no_nested_borrows.rs', lines 239:0-239:22 *)
 Definition test_copy_int : result unit :=
-  y <- copy_int 0%i32; if negb (0%i32 s= y) then Fail_ Failure else Return tt
+  y <- copy_int 0%i32; if negb (0%i32 s= y) then Fail_ Failure else Ok tt
 .
 
 (** Unit test for [no_nested_borrows::test_copy_int] *)
@@ -283,14 +283,14 @@ Check (test_copy_int )%return.
 (** [no_nested_borrows::is_cons]:
     Source: 'src/no_nested_borrows.rs', lines 246:0-246:38 *)
 Definition is_cons (T : Type) (l : List_t T) : result bool :=
-  match l with | List_Cons _ _ => Return true | List_Nil => Return false end
+  match l with | List_Cons _ _ => Ok true | List_Nil => Ok false end
 .
 
 (** [no_nested_borrows::test_is_cons]:
     Source: 'src/no_nested_borrows.rs', lines 253:0-253:21 *)
 Definition test_is_cons : result unit :=
   b <- is_cons i32 (List_Cons 0%i32 List_Nil);
-  if negb b then Fail_ Failure else Return tt
+  if negb b then Fail_ Failure else Ok tt
 .
 
 (** Unit test for [no_nested_borrows::test_is_cons] *)
@@ -299,10 +299,7 @@ Check (test_is_cons )%return.
 (** [no_nested_borrows::split_list]:
     Source: 'src/no_nested_borrows.rs', lines 259:0-259:48 *)
 Definition split_list (T : Type) (l : List_t T) : result (T * (List_t T)) :=
-  match l with
-  | List_Cons hd tl => Return (hd, tl)
-  | List_Nil => Fail_ Failure
-  end
+  match l with | List_Cons hd tl => Ok (hd, tl) | List_Nil => Fail_ Failure end
 .
 
 (** [no_nested_borrows::test_split_list]:
@@ -310,7 +307,7 @@ Definition split_list (T : Type) (l : List_t T) : result (T * (List_t T)) :=
 Definition test_split_list : result unit :=
   p <- split_list i32 (List_Cons 0%i32 List_Nil);
   let (hd, _) := p in
-  if negb (hd s= 0%i32) then Fail_ Failure else Return tt
+  if negb (hd s= 0%i32) then Fail_ Failure else Ok tt
 .
 
 (** Unit test for [no_nested_borrows::test_split_list] *)
@@ -321,8 +318,8 @@ Check (test_split_list )%return.
 Definition choose
   (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
   if b
-  then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
-  else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
+  then let back := fun (ret : T) => Ok (ret, y) in Ok (x, back)
+  else let back := fun (ret : T) => Ok (x, ret) in Ok (y, back)
 .
 
 (** [no_nested_borrows::choose_test]:
@@ -338,7 +335,7 @@ Definition choose_test : result unit :=
     let (x, y) := p1 in
     if negb (x s= 1%i32)
     then Fail_ Failure
-    else if negb (y s= 0%i32) then Fail_ Failure else Return tt)
+    else if negb (y s= 0%i32) then Fail_ Failure else Ok tt)
 .
 
 (** Unit test for [no_nested_borrows::choose_test] *)
@@ -347,7 +344,7 @@ Check (choose_test )%return.
 (** [no_nested_borrows::test_char]:
     Source: 'src/no_nested_borrows.rs', lines 294:0-294:26 *)
 Definition test_char : result char :=
-  Return (char_of_byte Coq.Init.Byte.x61).
+  Ok (char_of_byte Coq.Init.Byte.x61).
 
 (** [no_nested_borrows::Tree]
     Source: 'src/no_nested_borrows.rs', lines 299:0-299:16 *)
@@ -373,7 +370,7 @@ Arguments NodeElem_Nil { _ }.
 Fixpoint list_length (T : Type) (l : List_t T) : result u32 :=
   match l with
   | List_Cons _ l1 => i <- list_length T l1; u32_add 1%u32 i
-  | List_Nil => Return 0%u32
+  | List_Nil => Ok 0%u32
   end
 .
 
@@ -383,7 +380,7 @@ Fixpoint list_nth_shared (T : Type) (l : List_t T) (i : u32) : result T :=
   match l with
   | List_Cons x tl =>
     if i s= 0%u32
-    then Return x
+    then Ok x
     else (i1 <- u32_sub i 1%u32; list_nth_shared T tl i1)
   | List_Nil => Fail_ Failure
   end
@@ -398,17 +395,14 @@ Fixpoint list_nth_mut
   match l with
   | List_Cons x tl =>
     if i s= 0%u32
-    then
-      let back := fun (ret : T) => Return (List_Cons ret tl) in
-      Return (x, back)
+    then let back := fun (ret : T) => Ok (List_Cons ret tl) in Ok (x, back)
     else (
       i1 <- u32_sub i 1%u32;
       p <- list_nth_mut T tl i1;
       let (t, list_nth_mut_back) := p in
       let back :=
-        fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (List_Cons x tl1)
-        in
-      Return (t, back))
+        fun (ret : T) => tl1 <- list_nth_mut_back ret; Ok (List_Cons x tl1) in
+      Ok (t, back))
   | List_Nil => Fail_ Failure
   end
 .
@@ -419,7 +413,7 @@ Fixpoint list_rev_aux
   (T : Type) (li : List_t T) (lo : List_t T) : result (List_t T) :=
   match li with
   | List_Cons hd tl => list_rev_aux T tl (List_Cons hd lo)
-  | List_Nil => Return lo
+  | List_Nil => Ok lo
   end
 .
 
@@ -463,7 +457,7 @@ Definition test_list_functions : result unit :=
             then Fail_ Failure
             else (
               i6 <- list_nth_shared i32 ls 2%u32;
-              if negb (i6 s= 2%i32) then Fail_ Failure else Return tt))))))
+              if negb (i6 s= 2%i32) then Fail_ Failure else Ok tt))))))
 .
 
 (** Unit test for [no_nested_borrows::test_list_functions] *)
@@ -475,7 +469,7 @@ Definition id_mut_pair1
   (T1 T2 : Type) (x : T1) (y : T2) :
   result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
   :=
-  Return ((x, y), Return)
+  Ok ((x, y), Ok)
 .
 
 (** [no_nested_borrows::id_mut_pair2]:
@@ -484,7 +478,7 @@ Definition id_mut_pair2
   (T1 T2 : Type) (p : (T1 * T2)) :
   result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
   :=
-  let (t, t1) := p in Return ((t, t1), Return)
+  let (t, t1) := p in Ok ((t, t1), Ok)
 .
 
 (** [no_nested_borrows::id_mut_pair3]:
@@ -493,7 +487,7 @@ Definition id_mut_pair3
   (T1 T2 : Type) (x : T1) (y : T2) :
   result ((T1 * T2) * (T1 -> result T1) * (T2 -> result T2))
   :=
-  Return ((x, y), Return, Return)
+  Ok ((x, y), Ok, Ok)
 .
 
 (** [no_nested_borrows::id_mut_pair4]:
@@ -502,7 +496,7 @@ Definition id_mut_pair4
   (T1 T2 : Type) (p : (T1 * T2)) :
   result ((T1 * T2) * (T1 -> result T1) * (T2 -> result T2))
   :=
-  let (t, t1) := p in Return ((t, t1), Return, Return)
+  let (t, t1) := p in Ok ((t, t1), Ok, Ok)
 .
 
 (** [no_nested_borrows::StructWithTuple]
@@ -519,19 +513,19 @@ Arguments structWithTuple_p { _ _ }.
 (** [no_nested_borrows::new_tuple1]:
     Source: 'src/no_nested_borrows.rs', lines 437:0-437:48 *)
 Definition new_tuple1 : result (StructWithTuple_t u32 u32) :=
-  Return {| structWithTuple_p := (1%u32, 2%u32) |}
+  Ok {| structWithTuple_p := (1%u32, 2%u32) |}
 .
 
 (** [no_nested_borrows::new_tuple2]:
     Source: 'src/no_nested_borrows.rs', lines 441:0-441:48 *)
 Definition new_tuple2 : result (StructWithTuple_t i16 i16) :=
-  Return {| structWithTuple_p := (1%i16, 2%i16) |}
+  Ok {| structWithTuple_p := (1%i16, 2%i16) |}
 .
 
 (** [no_nested_borrows::new_tuple3]:
     Source: 'src/no_nested_borrows.rs', lines 445:0-445:48 *)
 Definition new_tuple3 : result (StructWithTuple_t u64 i64) :=
-  Return {| structWithTuple_p := (1%u64, 2%i64) |}
+  Ok {| structWithTuple_p := (1%u64, 2%i64) |}
 .
 
 (** [no_nested_borrows::StructWithPair]
@@ -548,7 +542,7 @@ Arguments structWithPair_p { _ _ }.
 (** [no_nested_borrows::new_pair1]:
     Source: 'src/no_nested_borrows.rs', lines 454:0-454:46 *)
 Definition new_pair1 : result (StructWithPair_t u32 u32) :=
-  Return {| structWithPair_p := {| pair_x := 1%u32; pair_y := 2%u32 |} |}
+  Ok {| structWithPair_p := {| pair_x := 1%u32; pair_y := 2%u32 |} |}
 .
 
 (** [no_nested_borrows::test_constants]:
@@ -572,7 +566,7 @@ Definition test_constants : result unit :=
         swp <- new_pair1;
         if negb (swp.(structWithPair_p).(pair_x) s= 1%u32)
         then Fail_ Failure
-        else Return tt)))
+        else Ok tt)))
 .
 
 (** Unit test for [no_nested_borrows::test_constants] *)
@@ -581,7 +575,7 @@ Check (test_constants )%return.
 (** [no_nested_borrows::test_weird_borrows1]:
     Source: 'src/no_nested_borrows.rs', lines 471:0-471:28 *)
 Definition test_weird_borrows1 : result unit :=
-  Return tt.
+  Ok tt.
 
 (** Unit test for [no_nested_borrows::test_weird_borrows1] *)
 Check (test_weird_borrows1 )%return.
@@ -590,30 +584,30 @@ Check (test_weird_borrows1 )%return.
     Source: 'src/no_nested_borrows.rs', lines 481:0-481:37 *)
 Definition test_mem_replace (px : u32) : result u32 :=
   let (y, _) := core_mem_replace u32 px 1%u32 in
-  if negb (y s= 0%u32) then Fail_ Failure else Return 2%u32
+  if negb (y s= 0%u32) then Fail_ Failure else Ok 2%u32
 .
 
 (** [no_nested_borrows::test_shared_borrow_bool1]:
     Source: 'src/no_nested_borrows.rs', lines 488:0-488:47 *)
 Definition test_shared_borrow_bool1 (b : bool) : result u32 :=
-  if b then Return 0%u32 else Return 1%u32
+  if b then Ok 0%u32 else Ok 1%u32
 .
 
 (** [no_nested_borrows::test_shared_borrow_bool2]:
     Source: 'src/no_nested_borrows.rs', lines 501:0-501:40 *)
 Definition test_shared_borrow_bool2 : result u32 :=
-  Return 0%u32.
+  Ok 0%u32.
 
 (** [no_nested_borrows::test_shared_borrow_enum1]:
     Source: 'src/no_nested_borrows.rs', lines 516:0-516:52 *)
 Definition test_shared_borrow_enum1 (l : List_t u32) : result u32 :=
-  match l with | List_Cons _ _ => Return 1%u32 | List_Nil => Return 0%u32 end
+  match l with | List_Cons _ _ => Ok 1%u32 | List_Nil => Ok 0%u32 end
 .
 
 (** [no_nested_borrows::test_shared_borrow_enum2]:
     Source: 'src/no_nested_borrows.rs', lines 528:0-528:40 *)
 Definition test_shared_borrow_enum2 : result u32 :=
-  Return 0%u32.
+  Ok 0%u32.
 
 (** [no_nested_borrows::incr]:
     Source: 'src/no_nested_borrows.rs', lines 539:0-539:24 *)
@@ -628,7 +622,7 @@ Definition call_incr (x : u32) : result u32 :=
 (** [no_nested_borrows::read_then_incr]:
     Source: 'src/no_nested_borrows.rs', lines 548:0-548:41 *)
 Definition read_then_incr (x : u32) : result (u32 * u32) :=
-  x1 <- u32_add x 1%u32; Return (x, x1)
+  x1 <- u32_add x 1%u32; Ok (x, x1)
 .
 
 (** [no_nested_borrows::Tuple]
@@ -638,14 +632,14 @@ Definition Tuple_t (T1 T2 : Type) : Type := T1 * T2.
 (** [no_nested_borrows::use_tuple_struct]:
     Source: 'src/no_nested_borrows.rs', lines 556:0-556:48 *)
 Definition use_tuple_struct (x : Tuple_t u32 u32) : result (Tuple_t u32 u32) :=
-  let (_, i) := x in Return (1%u32, i)
+  let (_, i) := x in Ok (1%u32, i)
 .
 
 (** [no_nested_borrows::create_tuple_struct]:
     Source: 'src/no_nested_borrows.rs', lines 560:0-560:61 *)
 Definition create_tuple_struct
   (x : u32) (y : u64) : result (Tuple_t u32 u64) :=
-  Return (x, y)
+  Ok (x, y)
 .
 
 (** [no_nested_borrows::IdType]
@@ -655,11 +649,11 @@ Definition IdType_t (T : Type) : Type := T.
 (** [no_nested_borrows::use_id_type]:
     Source: 'src/no_nested_borrows.rs', lines 567:0-567:40 *)
 Definition use_id_type (T : Type) (x : IdType_t T) : result T :=
-  Return x.
+  Ok x.
 
 (** [no_nested_borrows::create_id_type]:
     Source: 'src/no_nested_borrows.rs', lines 571:0-571:43 *)
 Definition create_id_type (T : Type) (x : T) : result (IdType_t T) :=
-  Return x.
+  Ok x.
 
 End NoNestedBorrows.
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 77276223..5995de15 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -16,7 +16,7 @@ Definition ref_incr (x : i32) : result i32 :=
 (** [paper::test_incr]:
     Source: 'src/paper.rs', lines 8:0-8:18 *)
 Definition test_incr : result unit :=
-  x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt
+  x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Ok tt
 .
 
 (** Unit test for [paper::test_incr] *)
@@ -27,8 +27,8 @@ Check (test_incr )%return.
 Definition choose
   (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
   if b
-  then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
-  else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
+  then let back := fun (ret : T) => Ok (ret, y) in Ok (x, back)
+  else let back := fun (ret : T) => Ok (x, ret) in Ok (y, back)
 .
 
 (** [paper::test_choose]:
@@ -44,7 +44,7 @@ Definition test_choose : result unit :=
     let (x, y) := p1 in
     if negb (x s= 1%i32)
     then Fail_ Failure
-    else if negb (y s= 0%i32) then Fail_ Failure else Return tt)
+    else if negb (y s= 0%i32) then Fail_ Failure else Ok tt)
 .
 
 (** Unit test for [paper::test_choose] *)
@@ -69,17 +69,14 @@ Fixpoint list_nth_mut
   match l with
   | List_Cons x tl =>
     if i s= 0%u32
-    then
-      let back := fun (ret : T) => Return (List_Cons ret tl) in
-      Return (x, back)
+    then let back := fun (ret : T) => Ok (List_Cons ret tl) in Ok (x, back)
     else (
       i1 <- u32_sub i 1%u32;
       p <- list_nth_mut T tl i1;
       let (t, list_nth_mut_back) := p in
       let back :=
-        fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (List_Cons x tl1)
-        in
-      Return (t, back))
+        fun (ret : T) => tl1 <- list_nth_mut_back ret; Ok (List_Cons x tl1) in
+      Ok (t, back))
   | List_Nil => Fail_ Failure
   end
 .
@@ -89,7 +86,7 @@ Fixpoint list_nth_mut
 Fixpoint sum (l : List_t i32) : result i32 :=
   match l with
   | List_Cons x tl => i <- sum tl; i32_add x i
-  | List_Nil => Return 0%i32
+  | List_Nil => Ok 0%i32
   end
 .
 
@@ -103,7 +100,7 @@ Definition test_nth : result unit :=
   x1 <- i32_add x 1%i32;
   l2 <- list_nth_mut_back x1;
   i <- sum l2;
-  if negb (i s= 7%i32) then Fail_ Failure else Return tt
+  if negb (i s= 7%i32) then Fail_ Failure else Ok tt
 .
 
 (** Unit test for [paper::test_nth] *)
@@ -118,7 +115,7 @@ Definition call_choose (p : (u32 * u32)) : result u32 :=
   pz1 <- u32_add pz 1%u32;
   p2 <- choose_back pz1;
   let (px1, _) := p2 in
-  Return px1
+  Ok px1
 .
 
 End Paper.
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index dfa09328..8af7f69c 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -27,15 +27,15 @@ Fixpoint get_list_at_x
   match ls with
   | List_Cons hd tl =>
     if hd s= x
-    then Return (List_Cons hd tl, Return)
+    then Ok (List_Cons hd tl, Ok)
     else (
       p <- get_list_at_x tl x;
       let (l, get_list_at_x_back) := p in
       let back :=
         fun (ret : List_t u32) =>
-          tl1 <- get_list_at_x_back ret; Return (List_Cons hd tl1) in
-      Return (l, back))
-  | List_Nil => Return (List_Nil, Return)
+          tl1 <- get_list_at_x_back ret; Ok (List_Cons hd tl1) in
+      Ok (l, back))
+  | List_Nil => Ok (List_Nil, Ok)
   end
 .
 
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
   | OutOfFuel.
 
 Inductive result A :=
-  | Return : A -> result A
+  | Ok : A -> result A
   | Fail_ : error -> result A.
 
-Arguments Return {_} a.
+Arguments Ok {_} a.
 Arguments Fail_ {_}.
 
 Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
   match m with
   | Fail_ e => Fail_ e
-  | Return x => f x
+  | Ok x => f x
   end.
 
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
 Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
 
 Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
 
 (** Monadic assert *)
 Definition massert (b: bool) : result unit :=
-  if b then Return tt else Fail_ Failure.
+  if b then Ok tt else Fail_ Failure.
 
 (** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
-  match a as r return (r = Return x -> A) with
-  | Return a' => fun _  => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+  match a as r return (r = Ok x -> A) with
+  | Ok a' => fun _  => a'
   | Fail_ e   => fun p' =>
       False_rect _ (eq_ind (Fail_ e)
           (fun e : result A =>
           match e with
-          | Return _ => False
+          | Ok _ => False
           | Fail_ e => True
           end)
-        I (Return x) p')
+        I (Ok x) p')
   end p.
 
 Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
 Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
 
 (* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
 
 (*** Misc *)
 
@@ -236,7 +236,7 @@ Import Sumbool.
 
 Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
   match sumbool_of_bool (scalar_in_bounds ty x) with
-  | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+  | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
 
 (*** [alloc] *)
 
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
 Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
-  Return (x, fun x => Return x).
+  Ok (x, fun x => Ok x).
 
 (* Trait instance *)
 Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
   result (T * (T -> result (array T n))) :=
   match array_index_usize T n a i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_update_usize T n a i)
+  | Ok x => Ok (x, array_update_usize T n a i)
   end.
 
 (*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
   result (T * (T -> result (slice T))) :=
   match slice_index_usize T s i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, slice_update_usize T s i)
+  | Ok x => Ok (x, slice_update_usize T s i)
   end.
 
 (*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
   result (slice T * (slice T -> result (array T n))) :=
   match array_to_slice T n a with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_from_slice T n a)
+  | Ok x => Ok (x, array_from_slice T n a)
   end.
 
 Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
 Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
   l <- f (alloc_vec_Vec_to_list v) ;
   match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
-  | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+  | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
 Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
-  alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+  alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
 
 Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
   alloc_vec_Vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
-    then Return (list_update l (usize_to_nat i) x)
+    then Ok (list_update l (usize_to_nat i) x)
     else Fail_ Failure).
 
 (* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
 Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
   result (T * (T -> result (alloc_vec_Vec T))) :=
   match alloc_vec_Vec_index_usize v i with
-  | Return x =>
-    Return (x, alloc_vec_Vec_update_usize v i)
+  | Ok x =>
+    Ok (x, alloc_vec_Vec_update_usize v i)
   | Fail_ e => Fail_ e
   end.
 
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
   x <- inst.(core_slice_index_SliceIndex_get) i s;
   match x with
   | None => Fail_ Failure
-  | Some x => Return x
+  | Some x => Ok x
   end.
 
 (* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/traits/Primitives.v b/tests/coq/traits/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/traits/Primitives.v
+++ b/tests/coq/traits/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
   | OutOfFuel.
 
 Inductive result A :=
-  | Return : A -> result A
+  | Ok : A -> result A
   | Fail_ : error -> result A.
 
-Arguments Return {_} a.
+Arguments Ok {_} a.
 Arguments Fail_ {_}.
 
 Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
   match m with
   | Fail_ e => Fail_ e
-  | Return x => f x
+  | Ok x => f x
   end.
 
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
 Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
 
 Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
 
 (** Monadic assert *)
 Definition massert (b: bool) : result unit :=
-  if b then Return tt else Fail_ Failure.
+  if b then Ok tt else Fail_ Failure.
 
 (** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
-  match a as r return (r = Return x -> A) with
-  | Return a' => fun _  => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+  match a as r return (r = Ok x -> A) with
+  | Ok a' => fun _  => a'
   | Fail_ e   => fun p' =>
       False_rect _ (eq_ind (Fail_ e)
           (fun e : result A =>
           match e with
-          | Return _ => False
+          | Ok _ => False
           | Fail_ e => True
           end)
-        I (Return x) p')
+        I (Ok x) p')
   end p.
 
 Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
 Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
 
 (* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
 
 (*** Misc *)
 
@@ -236,7 +236,7 @@ Import Sumbool.
 
 Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
   match sumbool_of_bool (scalar_in_bounds ty x) with
-  | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+  | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
 
 (*** [alloc] *)
 
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
 Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
-  Return (x, fun x => Return x).
+  Ok (x, fun x => Ok x).
 
 (* Trait instance *)
 Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
   result (T * (T -> result (array T n))) :=
   match array_index_usize T n a i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_update_usize T n a i)
+  | Ok x => Ok (x, array_update_usize T n a i)
   end.
 
 (*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
   result (T * (T -> result (slice T))) :=
   match slice_index_usize T s i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, slice_update_usize T s i)
+  | Ok x => Ok (x, slice_update_usize T s i)
   end.
 
 (*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
   result (slice T * (slice T -> result (array T n))) :=
   match array_to_slice T n a with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_from_slice T n a)
+  | Ok x => Ok (x, array_from_slice T n a)
   end.
 
 Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
 Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
   l <- f (alloc_vec_Vec_to_list v) ;
   match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
-  | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+  | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
 Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
-  alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+  alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
 
 Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
   alloc_vec_Vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
-    then Return (list_update l (usize_to_nat i) x)
+    then Ok (list_update l (usize_to_nat i) x)
     else Fail_ Failure).
 
 (* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
 Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
   result (T * (T -> result (alloc_vec_Vec T))) :=
   match alloc_vec_Vec_index_usize v i with
-  | Return x =>
-    Return (x, alloc_vec_Vec_update_usize v i)
+  | Ok x =>
+    Ok (x, alloc_vec_Vec_update_usize v i)
   | Fail_ e => Fail_ e
   end.
 
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
   x <- inst.(core_slice_index_SliceIndex_get) i s;
   match x with
   | None => Fail_ Failure
-  | Some x => Return x
+  | Some x => Ok x
   end.
 
 (* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 0e942c7d..fb37a507 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -20,7 +20,7 @@ Arguments BoolTrait_t_get_bool { _ }.
 (** [traits::{(traits::BoolTrait for bool)}::get_bool]:
     Source: 'src/traits.rs', lines 12:4-12:30 *)
 Definition boolTraitBool_get_bool (self : bool) : result bool :=
-  Return self.
+  Ok self.
 
 (** Trait implementation: [traits::{(traits::BoolTrait for bool)}]
     Source: 'src/traits.rs', lines 11:0-11:23 *)
@@ -32,21 +32,21 @@ Definition BoolTraitBool : BoolTrait_t bool := {|
     Source: 'src/traits.rs', lines 6:4-6:30 *)
 Definition boolTrait_ret_true
   {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool :=
-  Return true
+  Ok true
 .
 
 (** [traits::test_bool_trait_bool]:
     Source: 'src/traits.rs', lines 17:0-17:44 *)
 Definition test_bool_trait_bool (x : bool) : result bool :=
   b <- boolTraitBool_get_bool x;
-  if b then boolTrait_ret_true BoolTraitBool x else Return false
+  if b then boolTrait_ret_true BoolTraitBool x else Ok false
 .
 
 (** [traits::{(traits::BoolTrait for core::option::Option<T>)#1}::get_bool]:
     Source: 'src/traits.rs', lines 23:4-23:30 *)
 Definition boolTraitOption_get_bool
   (T : Type) (self : option T) : result bool :=
-  match self with | None => Return false | Some _ => Return true end
+  match self with | None => Ok false | Some _ => Ok true end
 .
 
 (** Trait implementation: [traits::{(traits::BoolTrait for core::option::Option<T>)#1}]
@@ -59,7 +59,7 @@ Definition BoolTraitOption (T : Type) : BoolTrait_t (option T) := {|
     Source: 'src/traits.rs', lines 31:0-31:54 *)
 Definition test_bool_trait_option (T : Type) (x : option T) : result bool :=
   b <- boolTraitOption_get_bool T x;
-  if b then boolTrait_ret_true (BoolTraitOption T) x else Return false
+  if b then boolTrait_ret_true (BoolTraitOption T) x else Ok false
 .
 
 (** [traits::test_bool_trait]:
@@ -81,7 +81,7 @@ Arguments ToU64_t_to_u64 { _ }.
 (** [traits::{(traits::ToU64 for u64)#2}::to_u64]:
     Source: 'src/traits.rs', lines 44:4-44:26 *)
 Definition toU64U64_to_u64 (self : u64) : result u64 :=
-  Return self.
+  Ok self.
 
 (** Trait implementation: [traits::{(traits::ToU64 for u64)#2}]
     Source: 'src/traits.rs', lines 43:0-43:18 *)
@@ -167,7 +167,7 @@ Arguments ToType_t_to_type { _ _ }.
 (** [traits::{(traits::ToType<bool> for u64)#5}::to_type]:
     Source: 'src/traits.rs', lines 93:4-93:28 *)
 Definition toTypeU64Bool_to_type (self : u64) : result bool :=
-  Return (self s> 0%u64)
+  Ok (self s> 0%u64)
 .
 
 (** Trait implementation: [traits::{(traits::ToType<bool> for u64)#5}]
@@ -238,7 +238,7 @@ Arguments TestType_test_TestTrait_t_test { _ }.
     Source: 'src/traits.rs', lines 139:12-139:34 *)
 Definition testType_test_TestTraittraitsTestTypetestTestType1_test
   (self : TestType_test_TestType1_t) : result bool :=
-  Return (self s> 1%u64)
+  Ok (self s> 1%u64)
 .
 
 (** Trait implementation: [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}]
@@ -258,7 +258,7 @@ Definition testType_test
   x1 <- toU64Inst.(ToU64_t_to_u64) x;
   if x1 s> 0%u64
   then testType_test_TestTraittraitsTestTypetestTestType1_test 0%u64
-  else Return false
+  else Ok false
 .
 
 (** [traits::BoolWrapper]
@@ -285,7 +285,7 @@ Definition ToTypetraitsBoolWrapperT (T : Type) (toTypeBoolTInst : ToType_t bool
     Source: 'src/traits.rs', lines 164:4-164:21 *)
 Definition with_const_ty_len2_default_body (Self : Type) (LEN : usize)
   : result usize :=
-  Return 32%usize
+  Ok 32%usize
 .
 Definition with_const_ty_len2_default (Self : Type) (LEN : usize) : usize :=
   (with_const_ty_len2_default_body Self LEN)%global
@@ -313,7 +313,7 @@ Arguments WithConstTy_t_f { _ _ }.
 
 (** [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
     Source: 'src/traits.rs', lines 175:4-175:21 *)
-Definition with_const_ty_bool32_len1_body : result usize := Return 12%usize.
+Definition with_const_ty_bool32_len1_body : result usize := Ok 12%usize.
 Definition with_const_ty_bool32_len1 : usize :=
   with_const_ty_bool32_len1_body%global
 .
@@ -322,7 +322,7 @@ Definition with_const_ty_bool32_len1 : usize :=
     Source: 'src/traits.rs', lines 180:4-180:39 *)
 Definition withConstTyBool32_f
   (i : u64) (a : array u8 32%usize) : result u64 :=
-  Return i
+  Ok i
 .
 
 (** Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}]
@@ -342,7 +342,7 @@ Definition use_with_const_ty1
   (H : Type) (LEN : usize) (withConstTyInst : WithConstTy_t H LEN) :
   result usize
   :=
-  Return withConstTyInst.(WithConstTy_tWithConstTy_t_LEN1)
+  Ok withConstTyInst.(WithConstTy_tWithConstTy_t_LEN1)
 .
 
 (** [traits::use_with_const_ty2]:
@@ -352,7 +352,7 @@ Definition use_with_const_ty2
   (w : withConstTyInst.(WithConstTy_tWithConstTy_t_W)) :
   result unit
   :=
-  Return tt
+  Ok tt
 .
 
 (** [traits::use_with_const_ty3]:
@@ -368,7 +368,7 @@ Definition use_with_const_ty3
 (** [traits::test_where1]:
     Source: 'src/traits.rs', lines 193:0-193:40 *)
 Definition test_where1 (T : Type) (_x : T) : result unit :=
-  Return tt.
+  Ok tt.
 
 (** [traits::test_where2]:
     Source: 'src/traits.rs', lines 194:0-194:57 *)
@@ -376,7 +376,7 @@ Definition test_where2
   (T : Type) (withConstTyT32Inst : WithConstTy_t T 32%usize) (_x : u32) :
   result unit
   :=
-  Return tt
+  Ok tt
 .
 
 (** Trait declaration: [traits::ParentTrait0]
@@ -435,7 +435,7 @@ Definition order1
   ParentTrait0_t U) :
   result unit
   :=
-  Return tt
+  Ok tt
 .
 
 (** Trait declaration: [traits::ChildTrait1]
@@ -552,7 +552,7 @@ Definition ParentTrait2U32 : ParentTrait2_t u32 := {|
 (** [traits::{(traits::ChildTrait2 for u32)#13}::convert]:
     Source: 'src/traits.rs', lines 273:4-273:29 *)
 Definition childTrait2U32_convert (x : u32) : result u32 :=
-  Return x.
+  Ok x.
 
 (** Trait implementation: [traits::{(traits::ChildTrait2 for u32)#13}]
     Source: 'src/traits.rs', lines 272:0-272:24 *)
@@ -625,9 +625,7 @@ Arguments Trait_tTrait_t_LEN { _ }.
 
 (** [traits::{(traits::Trait for @Array<T, N>)#14}::LEN]
     Source: 'src/traits.rs', lines 315:4-315:20 *)
-Definition trait_array_len_body (T : Type) (N : usize) : result usize :=
-  Return N
-.
+Definition trait_array_len_body (T : Type) (N : usize) : result usize := Ok N.
 Definition trait_array_len (T : Type) (N : usize) : usize :=
   (trait_array_len_body T N)%global
 .
@@ -642,7 +640,7 @@ Definition TraitArray (T : Type) (N : usize) : Trait_t (array T N) := {|
     Source: 'src/traits.rs', lines 319:4-319:20 *)
 Definition traittraits_wrapper_len_body (T : Type) (traitInst : Trait_t T)
   : result usize :=
-  Return 0%usize
+  Ok 0%usize
 .
 Definition traittraits_wrapper_len (T : Type) (traitInst : Trait_t T)
   : usize :=
@@ -659,7 +657,7 @@ Definition TraittraitsWrapper (T : Type) (traitInst : Trait_t T) : Trait_t
 (** [traits::use_wrapper_len]:
     Source: 'src/traits.rs', lines 322:0-322:43 *)
 Definition use_wrapper_len (T : Type) (traitInst : Trait_t T) : result usize :=
-  Return (TraittraitsWrapper T traitInst).(Trait_tTrait_t_LEN)
+  Ok (TraittraitsWrapper T traitInst).(Trait_tTrait_t_LEN)
 .
 
 (** [traits::Foo]
@@ -685,7 +683,7 @@ Arguments Core_result_Result_Err { _ _ }.
     Source: 'src/traits.rs', lines 332:4-332:33 *)
 Definition foo_foo_body (T U : Type) (traitInst : Trait_t T)
   : result (core_result_Result_t T i32) :=
-  Return (Core_result_Result_Err 0%i32)
+  Ok (Core_result_Result_Err 0%i32)
 .
 Definition foo_foo (T U : Type) (traitInst : Trait_t T)
   : core_result_Result_t T i32 :=
@@ -696,14 +694,14 @@ Definition foo_foo (T U : Type) (traitInst : Trait_t T)
     Source: 'src/traits.rs', lines 335:0-335:48 *)
 Definition use_foo1
   (T U : Type) (traitInst : Trait_t T) : result (core_result_Result_t T i32) :=
-  Return (foo_foo T U traitInst)
+  Ok (foo_foo T U traitInst)
 .
 
 (** [traits::use_foo2]:
     Source: 'src/traits.rs', lines 339:0-339:48 *)
 Definition use_foo2
   (T U : Type) (traitInst : Trait_t U) : result (core_result_Result_t U i32) :=
-  Return (foo_foo U T traitInst)
+  Ok (foo_foo U T traitInst)
 .
 
 End Traits.