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 /tactics/class_tactics.ml4 | |
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 'tactics/class_tactics.ml4')
-rw-r--r-- | tactics/class_tactics.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 3b193f6d9..3f4e773ec 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -79,6 +79,7 @@ let auto_unif_flags = { modulo_delta_types = full_transparent_state; resolve_evars = false; use_evars_pattern_unification = true; + frozen_evars = ExistentialSet.empty; modulo_betaiota = true; modulo_eta = true; allow_K_in_toplevel_higher_order_unification = false |