Changement de comportement du [rewrite ... in H]: Coq échoue si H

apparaît dans le but ou dans l'une des hypothèses (ferme les bugs
#447, #883 et #1228).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9201 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 26 insertions, 0 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7cb0cb5394..57043057a3 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -245,6 +245,31 @@ let global_vars_set env constr =
   in 
   filtrec Idset.empty constr
 
+(* like [global_vars] but don't get through evars *)
+let global_vars_set_drop_evar env constr = 
+  let fold_constr_drop_evar f acc c = match kind_of_term c with
+    | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+      | Construct _) -> acc
+    | Cast (c,_,t) -> f (f acc c) t
+    | Prod (_,t,c) -> f (f acc t) c
+    | Lambda (_,t,c) -> f (f acc t) c
+    | LetIn (_,b,t,c) -> f (f (f acc b) t) c
+    | App (c,l) -> Array.fold_left f (f acc c) l
+    | Evar (_,l) -> acc
+    | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
+    | Fix (_,(lna,tl,bl)) ->
+	let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in
+	  Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd
+    | CoFix (_,(lna,tl,bl)) ->
+	let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in
+	  Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd in
+  let rec filtrec acc c =
+    let vl = vars_of_global env c in
+    let acc = List.fold_right Idset.add vl acc in
+      fold_constr_drop_evar filtrec acc c
+  in 
+    filtrec Idset.empty constr
+
 (* [keep_hyps env ids] keeps the part of the section context of [env] which 
    contains the variables of the set [ids], and recursively the variables 
    contained in the types of the needed variables. *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 24e72b9a23..b6d9bf6d38 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -165,6 +165,7 @@ val set_engagement : engagement -> env -> env
 (* [global_vars_set env c] returns the list of [id]'s occurring as
    [VAR id] in [c] *)
 val global_vars_set : env -> constr -> Idset.t
+val global_vars_set_drop_evar : env -> constr -> Idset.t
 (* the constr must be an atomic construction *)
 val vars_of_global : env -> constr -> identifier list