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

10 files changed, 62 insertions, 14 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 9d3e4225db..5125b21cc1 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -495,6 +495,14 @@ let evar_list evd c =
     | _ -> fold_constr evrec acc c in
   evrec [] c
 
+let collect_evars c =
+  let rec collrec acc c =
+    match kind_of_term c with
+      | Evar (evk,_) -> ExistentialSet.add evk acc
+      | _       -> fold_constr collrec acc c
+  in
+  collrec ExistentialSet.empty c
+
 (**********************************************************)
 (* Sort variables *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index c0efdb9f82..8131837d81 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -200,8 +200,6 @@ val evar_source : existential_key -> evar_map -> hole_kind located
    [evar_merge evd ev1] extends the evars of [evd] with [evd1] *)
 val evar_merge : evar_map -> evar_map -> evar_map
 
-val evar_list : evar_map -> constr -> existential list
-
 (** Unification constraints *)
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * constr * constr
@@ -214,6 +212,8 @@ val extract_changed_conv_pbs : evar_map ->
       evar_map * evar_constraint list
 val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
 
+val evar_list : evar_map -> constr -> existential list
+val collect_evars : constr -> ExistentialSet.t
 
 (** Metas *)
 val find_meta : evar_map -> metavariable -> clbinding
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 47fec14963..d09e5f2451 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -163,6 +163,7 @@ type unify_flags = {
   modulo_delta_types : Names.transparent_state;
   resolve_evars : bool;
   use_evars_pattern_unification : bool;
+  frozen_evars : ExistentialSet.t;
   modulo_betaiota : bool;
   modulo_eta : bool;
   allow_K_in_toplevel_higher_order_unification : bool
@@ -175,6 +176,7 @@ let default_unify_flags = {
   modulo_delta_types = full_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = true;
+  frozen_evars = ExistentialSet.empty;
   modulo_betaiota = false;
   modulo_eta = true;
   allow_K_in_toplevel_higher_order_unification = false
@@ -187,6 +189,7 @@ let default_no_delta_unify_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
@@ -199,6 +202,7 @@ let elim_flags = {
   modulo_delta_types = full_transparent_state;
   resolve_evars = false;
   use_evars_pattern_unification = true;
+  frozen_evars = ExistentialSet.empty;
   modulo_betaiota = false;
   modulo_eta = true;
   allow_K_in_toplevel_higher_order_unification = true
@@ -211,6 +215,7 @@ let elim_no_delta_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 = true
@@ -251,6 +256,10 @@ let do_reduce env sigma c =
   let (t, l) = whd_betaiota_deltazeta_for_iota_state env sigma (c, empty_stack) in
     applist (t, list_of_stack l)
 
+let isAllowedEvar flags c = match kind_of_term c with
+  | Evar (evk,_) -> not (ExistentialSet.mem evk flags.frozen_evars)
+  | _ -> false
+
 let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
   let rec unirec_rec (curenv,nb as curenvnb) pb b ((sigma,metasubst,evarsubst) as substn) curm curn =
     let cM = Evarutil.whd_head_evar sigma curm
@@ -280,8 +289,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
               (sigma,(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst,
               evarsubst)
 	    else error_cannot_unify_local curenv sigma (m,n,cM)
-	| Evar ev, _ -> sigma,metasubst,((curenv, ev,cN)::evarsubst)
-	| _, Evar ev -> sigma,metasubst,((curenv, ev,cM)::evarsubst)
+	| Evar (evk,_ as ev), _
+            when not (ExistentialSet.mem evk flags.frozen_evars) ->
+            sigma,metasubst,((curenv, ev,cN)::evarsubst)
+	| _, Evar (evk,_ as ev)
+            when not (ExistentialSet.mem evk flags.frozen_evars) ->
+            sigma,metasubst,((curenv, ev,cM)::evarsubst)
 
 	| Sort s1, Sort s2 ->
 	    (try 
@@ -318,13 +331,15 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	       reduce curenvnb pb b substn cM cN)
 
 	| App (f1,l1), _ when
-	    (isMeta f1 || use_evars_pattern_unification flags && isEvar f1) &
+	    (isMeta f1 || use_evars_pattern_unification flags &&
+                          isAllowedEvar flags f1) &
 	    is_unification_pattern curenvnb f1 l1 cN &
 	    not (dependent f1 cN) ->
 	      solve_pattern_eqn_array curenvnb f1 l1 cN substn
 
 	| _, App (f2,l2) when
-	    (isMeta f2 || use_evars_pattern_unification flags && isEvar f2) &
+	    (isMeta f2 || use_evars_pattern_unification flags &&
+                          isAllowedEvar flags f2) &
 	    is_unification_pattern curenvnb f2 l2 cM &
 	    not (dependent f2 cM) ->
 	      solve_pattern_eqn_array curenvnb f2 l2 cM substn
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 0f7eec6925..aa0267698e 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -17,6 +17,7 @@ type unify_flags = {
   modulo_delta_types : Names.transparent_state;
   resolve_evars : bool;
   use_evars_pattern_unification : bool;
+  frozen_evars : ExistentialSet.t;
   modulo_betaiota : bool;
   modulo_eta : bool;
   allow_K_in_toplevel_higher_order_unification : bool
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
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 }
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index e5b6e41598..18ba0fc870 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -90,12 +90,14 @@ intros.
 apply H.
 Qed.
 
+(* Feature deactivated in commit 14189 (see commit log)
 (* Test instanciation of evars by unification *)
 
 Goal (forall x, 0 + x = 0 -> True) -> True.
 intros; eapply H.
 rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *)
 Abort.
+*)
 
 (* Check handling of identity equation between evars *)
 (* The example failed to pass until revision 10623 *)