summaryrefslogtreecommitdiff
path: root/tests/coq/misc
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq/misc')
-rw-r--r--tests/coq/misc/Constants.v6
-rw-r--r--tests/coq/misc/NoNestedBorrows.v8
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] *)