diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-12 22:27:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-12 22:27:38 +0000 |
| commit | 9d3bc8da6655f0a2d207014a38a0c7a1cf8a1788 (patch) | |
| tree | e30523f30bb15811f9d8e1a9e950a4832a1a2d9e /proofs/clenvtac.ml | |
| parent | a38fbefca61f3392efe0ba98adfbae138022cce4 (diff) | |
Added a new flag for freezing evars in tactic unification. Used this
flag to forbid rewriting tactics to instantiate an evar of the goal
while looking for subterms (this is not clear that we always want that
for rewrite but we certainly want it for autorewrite; see comments
by Charguéraud on coqdev Oct 2010).
In a few cases in the theories, a pre-existing evar of an hyp used for
rewriting is instantiated by the rewriting step. Let's accept this at
the current time.
We have to make progress towards documenting and stabilizing the
strategy for matching/unifying subterms in rewrite/induction/set...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14190 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index e05651952..dad4b5041 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -107,6 +107,7 @@ let fail_quick_unif_flags = { modulo_delta_types = full_transparent_state; resolve_evars = false; use_evars_pattern_unification = false; + frozen_evars = ExistentialSet.empty; modulo_betaiota = false; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = false |