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 | |
| 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')
| -rw-r--r-- | kernel/environ.ml | 24 | ||||
| -rw-r--r-- | kernel/environ.mli | 1 |
2 files changed, 0 insertions, 25 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 diff --git a/kernel/environ.mli b/kernel/environ.mli index 175b18b247..8ba5962d3b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -165,7 +165,6 @@ 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 |