diff options
| author | notin | 2007-02-01 19:13:34 +0000 |
|---|---|---|
| committer | notin | 2007-02-01 19:13:34 +0000 |
| commit | 41b1b3042d6e03324857d8fa6273470635598f92 (patch) | |
| tree | da2b0c326a7c75ff80bf6428f37ba4280dd41245 /kernel/environ.ml | |
| parent | 81fd137b585ad8b78794267269556b5439be31f1 (diff) | |
Suppression de code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9582 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 2d821991e0..56c0574888 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -245,30 +245,6 @@ 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 |