diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 17d79830..be9a214b 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1351,9 +1351,17 @@ end; (* We may have uncovered more conjunctions *) repeat match goal with H:and _ _ |- _ => destruct H end. +Ltac generalize_embedded_proofs := + repeat match goal with H:context [?X] |- _ => + match type of X with ArithFact _ => + generalize dependent X + end + end; + intros. Ltac prepare_for_solver := (*dump_context;*) + generalize_embedded_proofs; clear_irrelevant_defns; clear_non_Z_bool_defns; autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *) |