From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- kernel/environ.ml | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) (limited to 'kernel/environ.ml') 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. *) -- cgit v1.2.3