diff options
| author | herbelin | 2009-11-09 18:05:13 +0000 |
|---|---|---|
| committer | herbelin | 2009-11-09 18:05:13 +0000 |
| commit | 1a4a7fa6dbd7c43c5d6c99297d1b6c5c497c0589 (patch) | |
| tree | fc18af5b3330e830a8e979bc551db46b25bda05d /kernel | |
| parent | cb2f5d06481f9021f600eaefbdc6b33118bd346d (diff) | |
A bit of cleaning around name generation + creation of dedicated file namegen.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 12 | ||||
| -rw-r--r-- | kernel/environ.mli | 2 |
2 files changed, 9 insertions, 5 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index a233d0be19..8f6a619a0a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -221,13 +221,17 @@ let vars_of_global env constr = | Const kn -> lookup_constant_variables kn env | Ind ind -> lookup_inductive_variables ind env | Construct cstr -> lookup_constructor_variables cstr env - | _ -> [] + | _ -> raise Not_found let global_vars_set env constr = 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 filtrec acc c + let acc = + match kind_of_term c with + | Var _ | Const _ | Ind _ | Construct _ -> + List.fold_right Idset.add (vars_of_global env c) acc + | _ -> + acc in + fold_constr filtrec acc c in filtrec Idset.empty constr diff --git a/kernel/environ.mli b/kernel/environ.mli index 9401ba6b03..315bddd1f7 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -164,7 +164,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 -(* the constr must be an atomic construction *) +(* the constr must be a global reference *) val vars_of_global : env -> constr -> identifier list val keep_hyps : env -> Idset.t -> section_context |