2 files changed, 7 insertions, 7 deletions
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 0a72558d..cd3880c2 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -44,7 +44,7 @@ Arguments Pair_y {T1} {T2}.
 
 (** [constants::mk_pair1] *)
 Definition 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] *)
@@ -61,7 +61,7 @@ Definition p2_c : (u32 * u32) := p2_body%global.
 
 (** [constants::P3] *)
 Definition p3_body : result (Pair_t u32 u32) :=
-  Return (mkPair_t (0%u32) (1%u32))
+  Return {| Pair_x := (0%u32); Pair_y := (1%u32) |}
 .
 Definition p3_c : Pair_t u32 u32 := p3_body%global.
 
@@ -73,7 +73,7 @@ Arguments Wrap_val {T}.
 
 (** [constants::Wrap::{0}::new] *)
 Definition wrap_new_fwd (T : Type) (val : T) : result (Wrap_t T) :=
-  Return (mkWrap_t val)
+  Return {| Wrap_val := val |}
 .
 
 (** [constants::Y] *)
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 98ed1cf6..826b52b6 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -423,17 +423,17 @@ Arguments Struct_with_tuple_p {T1} {T2}.
 
 (** [no_nested_borrows::new_tuple1] *)
 Definition new_tuple1_fwd : result (Struct_with_tuple_t u32 u32) :=
-  Return (mkStruct_with_tuple_t (1%u32, 2%u32))
+  Return {| Struct_with_tuple_p := (1%u32, 2%u32) |}
 .
 
 (** [no_nested_borrows::new_tuple2] *)
 Definition new_tuple2_fwd : result (Struct_with_tuple_t i16 i16) :=
-  Return (mkStruct_with_tuple_t (1%i16, 2%i16))
+  Return {| Struct_with_tuple_p := (1%i16, 2%i16) |}
 .
 
 (** [no_nested_borrows::new_tuple3] *)
 Definition new_tuple3_fwd : result (Struct_with_tuple_t u64 i64) :=
-  Return (mkStruct_with_tuple_t (1%u64, 2%i64))
+  Return {| Struct_with_tuple_p := (1%u64, 2%i64) |}
 .
 
 (** [no_nested_borrows::StructWithPair] *)
@@ -448,7 +448,7 @@ Arguments Struct_with_pair_p {T1} {T2}.
 
 (** [no_nested_borrows::new_pair1] *)
 Definition new_pair1_fwd : result (Struct_with_pair_t u32 u32) :=
-  Return (mkStruct_with_pair_t (mkPair_t (1%u32) (2%u32)))
+  Return {| Struct_with_pair_p := {| Pair_x := (1%u32); Pair_y := (2%u32) |} |}
 .
 
 (** [no_nested_borrows::test_constants] *)