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

4 files changed, 29 insertions, 8 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4c00a60d00..6780ae2fcf 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -845,6 +845,7 @@ let auto_unif_flags = {
   modulo_delta_types = full_transparent_state;
   resolve_evars = true;
   use_evars_pattern_unification = false;
+  frozen_evars = ExistentialSet.empty;
   modulo_betaiota = false;
   modulo_eta = true;
   allow_K_in_toplevel_higher_order_unification = false
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 3b193f6d93..3f4e773eca 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
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3b734b4c64..f6e8837f8b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -87,12 +87,25 @@ let rewrite_unif_flags = {
   Unification.modulo_delta_types = empty_transparent_state;
   Unification.resolve_evars = true;
   Unification.use_evars_pattern_unification = true;
+  Unification.frozen_evars = ExistentialSet.empty;
   Unification.modulo_betaiota = false;
   Unification.modulo_eta = true;
   Unification.allow_K_in_toplevel_higher_order_unification = false
     (* allow_K does not matter in practice because calls w_typed_unify *)
 }
 
+let freeze_initial_evars sigma flags clause =
+  (* We take evars of the type: this may include old evars! For excluding *)
+  (* all old evars, including the ones occurring in the rewriting lemma, *)
+  (* we would have to take the clenv_value *)
+  let newevars = Evd.collect_evars (clenv_type clause) in
+  let evars =
+    fold_undefined (fun evk _ evars ->
+      if ExistentialSet.mem evk newevars then evars
+      else ExistentialSet.add evk evars)
+      sigma ExistentialSet.empty in
+  { flags with Unification.frozen_evars = evars }
+
 let side_tac tac sidetac =
   match sidetac with
   | None -> tac
@@ -110,8 +123,9 @@ let instantiate_lemma_all env sigma gl c ty l l2r concl =
   let try_occ (evd', c') =
     clenv_pose_dependent_evars true {eqclause with evd = evd'}
   in
+  let flags = freeze_initial_evars sigma rewrite_unif_flags eqclause in
   let occs =
-    Unification.w_unify_to_subterm_all ~flags:rewrite_unif_flags env
+    Unification.w_unify_to_subterm_all ~flags env
       ((if l2r then c1 else c2),concl) eqclause.evd
   in List.map try_occ occs
 
@@ -129,20 +143,22 @@ let rewrite_conv_closed_unif_flags = {
   Unification.modulo_delta_types = full_transparent_state;
   Unification.resolve_evars = false;
   Unification.use_evars_pattern_unification = true;
+  Unification.frozen_evars = ExistentialSet.empty;
   Unification.modulo_betaiota = false;
   Unification.modulo_eta = true;
   Unification.allow_K_in_toplevel_higher_order_unification = false
 }
 
-let rewrite_elim with_evars c e =
-  general_elim_clause_gen
-    (elimination_clause_scheme with_evars ~flags:rewrite_conv_closed_unif_flags)
-     c e
+let rewrite_elim with_evars c e gl =
+  let flags =
+    freeze_initial_evars (project gl) rewrite_conv_closed_unif_flags c in
+  general_elim_clause_gen (elimination_clause_scheme with_evars ~flags) c e gl
 
-let rewrite_elim_in with_evars id c e =
+let rewrite_elim_in with_evars id c e gl =
+  let flags =
+    freeze_initial_evars (project gl) rewrite_conv_closed_unif_flags c in
   general_elim_clause_gen
-    (elimination_in_clause_scheme with_evars
-       ~flags:rewrite_conv_closed_unif_flags id) c e
+    (elimination_in_clause_scheme with_evars ~flags id) c e gl
 
 (* Ad hoc asymmetric general_elim_clause *)
 let general_elim_clause with_evars cls rew elim =
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 41ed88d2f7..b8ebf84a61 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -307,6 +307,7 @@ let rewrite_unif_flags = {
   Unification.modulo_delta_types = full_transparent_state;
   Unification.resolve_evars = true;
   Unification.use_evars_pattern_unification = true;
+  Unification.frozen_evars = ExistentialSet.empty;
   Unification.modulo_betaiota = false;
   Unification.modulo_eta = true;
   Unification.allow_K_in_toplevel_higher_order_unification = true
@@ -319,6 +320,7 @@ let rewrite2_unif_flags =
      Unification.modulo_delta_types = conv_transparent_state;
      Unification.resolve_evars = true;
      Unification.use_evars_pattern_unification = true;
+     Unification.frozen_evars = ExistentialSet.empty;
      Unification.modulo_betaiota = true;
      Unification.modulo_eta = true;
      Unification.allow_K_in_toplevel_higher_order_unification = true
@@ -332,6 +334,7 @@ let general_rewrite_unif_flags () =
        Unification.modulo_delta_types = ts;
        Unification.resolve_evars = true;
        Unification.use_evars_pattern_unification = true;
+       Unification.frozen_evars = ExistentialSet.empty;
        Unification.modulo_betaiota = true;
        Unification.modulo_eta = true;
        Unification.allow_K_in_toplevel_higher_order_unification = true }