diff options
author | Son Ho | 2023-03-07 23:50:36 +0100 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | ca77353c20e425c687ba207023d56828de6495b6 (patch) | |
tree | 4a800459fb5ec27dcfb1f20e4d5d0d785bb07959 /tests/coq/misc/Constants.v | |
parent | fa76f1b94e1f68d520b02c0dc1072cb73fa9d8be (diff) |
Start updating simplify_aggregates
Diffstat (limited to '')
-rw-r--r-- | tests/coq/misc/Constants.v | 6 |
1 files changed, 3 insertions, 3 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] *) |