Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 26 insertions, 1 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index a1e19815..e73f5848 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: environ.ml 8810 2006-05-12 18:50:21Z barras $ *)
+(* $Id: environ.ml 9201 2006-10-03 16:47:40Z notin $ *)
 
 open Util
 open Names
@@ -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. *)