From 9d3bc8da6655f0a2d207014a38a0c7a1cf8a1788 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 12 Jun 2011 22:27:38 +0000
Subject: 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
---
 proofs/clenvtac.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofs')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index e056519523..dad4b5041e 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
-- 
cgit v1.2.3