Merge pull request #123 from AeneasVerif/son/clean

Cleanup the code in preparation of the nested loops

1 files changed, 17 insertions, 18 deletions

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.