Start updating simplify_aggregates

2 files changed, 7 insertions, 7 deletions

diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index bf13ad43..bf2f0b1b 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -38,7 +38,7 @@ type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
 
 (** [constants::mk_pair1] *)
 let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
-  Return (Mkpair_t x y)
+  Return { pair_x = x; pair_y = y }
 
 (** [constants::P0] *)
 let p0_body : result (u32 & u32) = mk_pair0_fwd 0 1
@@ -53,7 +53,7 @@ let p2_body : result (u32 & u32) = Return (0, 1)
 let p2_c : (u32 & u32) = eval_global p2_body
 
 (** [constants::P3] *)
-let p3_body : result (pair_t u32 u32) = Return (Mkpair_t 0 1)
+let p3_body : result (pair_t u32 u32) = Return { pair_x = 0; pair_y = 1 }
 let p3_c : pair_t u32 u32 = eval_global p3_body
 
 (** [constants::Wrap] *)
@@ -61,7 +61,7 @@ type wrap_t (t : Type0) = { wrap_val : t; }
 
 (** [constants::Wrap::{0}::new] *)
 let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
-  Return (Mkwrap_t val0)
+  Return { wrap_val = val0 }
 
 (** [constants::Y] *)
 let y_body : result (wrap_t i32) = wrap_new_fwd i32 2
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 1e186c79..3770ab5d 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -353,15 +353,15 @@ type struct_with_tuple_t (t1 t2 : Type0) = { struct_with_tuple_p : (t1 & t2); }
 
 (** [no_nested_borrows::new_tuple1] *)
 let new_tuple1_fwd : result (struct_with_tuple_t u32 u32) =
-  Return (Mkstruct_with_tuple_t (1, 2))
+  Return { struct_with_tuple_p = (1, 2) }
 
 (** [no_nested_borrows::new_tuple2] *)
 let new_tuple2_fwd : result (struct_with_tuple_t i16 i16) =
-  Return (Mkstruct_with_tuple_t (1, 2))
+  Return { struct_with_tuple_p = (1, 2) }
 
 (** [no_nested_borrows::new_tuple3] *)
 let new_tuple3_fwd : result (struct_with_tuple_t u64 i64) =
-  Return (Mkstruct_with_tuple_t (1, 2))
+  Return { struct_with_tuple_p = (1, 2) }
 
 (** [no_nested_borrows::StructWithPair] *)
 type struct_with_pair_t (t1 t2 : Type0) =
@@ -371,7 +371,7 @@ type struct_with_pair_t (t1 t2 : Type0) =
 
 (** [no_nested_borrows::new_pair1] *)
 let new_pair1_fwd : result (struct_with_pair_t u32 u32) =
-  Return (Mkstruct_with_pair_t (Mkpair_t 1 2))
+  Return { struct_with_pair_p = { pair_x = 1; pair_y = 2 } }
 
 (** [no_nested_borrows::test_constants] *)
 let test_constants_fwd : result unit =