diff options
| author | Brian Campbell | 2019-04-19 14:42:14 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-04-19 14:42:14 +0100 |
| commit | 59adf48b33e49ea07ee1ab0984be066f60115041 (patch) | |
| tree | a8e2f7db512a447b7103cc8e5c00ddc502c2de30 /lib/coq | |
| parent | 1908fc3a361a3e8f01e36310926440a031697f53 (diff) | |
Coq: more robust handling of unknown constraints
Diffstat (limited to 'lib/coq')
| -rw-r--r-- | lib/coq/Sail2_values.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 67b76416..8c9c40a3 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1225,9 +1225,10 @@ Ltac prepare_for_solver := unfold_In; (* after unbool_comparisons to deal with && and || *) reduce_list_lengths; reduce_pow; - (* omega doesn't cope well with extra "True"s in the goal *) - repeat setoid_rewrite True_left; - repeat setoid_rewrite True_right. + (* omega doesn't cope well with extra "True"s in the goal. + Check that they actually appear because setoid_rewrite can fill in evars. *) + repeat match goal with |- context[True /\ _] => setoid_rewrite True_left end; + repeat match goal with |- context[_ /\ True] => setoid_rewrite True_right end. Lemma trivial_range {x : Z} : ArithFact (x <= x /\ x <= x). constructor. @@ -1292,7 +1293,7 @@ prepare_for_solver; constructor; repeat match goal with |- and _ _ => split end; solve - [ match goal with |- (?x _) => is_evar x; idtac "Warning: unknown constraint"; exact (I : (fun _ => True) _) end + [ match goal with |- (?x ?y) => is_evar x; idtac "Warning: unknown constraint"; exact (I : (fun _ => True) y) end | apply ArithFact_mword; assumption | omega with Z (* Try sail hints before dropping the existential *) |