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, 30 insertions, 6 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