Regenerate the test files

8 files changed, 165 insertions, 185 deletions

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/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 *)