diff options
| -rw-r--r-- | lib/coq/Sail2_values.v | 9 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 6 |
2 files changed, 14 insertions, 1 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 37e75961..b7e9bbc9 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1125,6 +1125,10 @@ repeat end. *) +(* The linear solver doesn't like existentials. *) +Ltac destruct_exists := + repeat match goal with H:@ex Z _ |- _ => destruct H end. + Ltac prepare_for_solver := (*dump_context;*) clear_irrelevant_defns; @@ -1134,6 +1138,7 @@ Ltac prepare_for_solver := extract_properties; repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end; unwrap_ArithFacts; + destruct_exists; unbool_comparisons; unfold_In; (* after unbool_comparisons to deal with && and || *) reduce_list_lengths; @@ -1798,3 +1803,7 @@ Definition sub_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} : Definition min_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} : {z : Z & ArithFact (z >= 0)} := build_ex (Z.min x y). + +Definition max_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} : + {z : Z & ArithFact (z >= 0)} := + build_ex (Z.max x y). diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 18e288dd..4f6a0dfc 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1383,7 +1383,11 @@ let doc_exp, doc_let = if effects then if inner_ex then if cast_ex - then string "derive_m" ^^ space ^^ epp + (* If the types are the same use the cast as a hint to Coq, + otherwise derive the new type from the old one. *) + then if alpha_equivalent env inner_typ cast_typ + then epp + else string "derive_m" ^^ space ^^ epp else string "projT1_m" ^^ space ^^ epp else if cast_ex then string "build_ex_m" ^^ space ^^ epp |