Coq: generalize proof terms before main solver

Ensures that dependencies in proofs don't affect rewriting.

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 *)