From 1a4a7fa6dbd7c43c5d6c99297d1b6c5c497c0589 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 9 Nov 2009 18:05:13 +0000
Subject: 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
---
 kernel/environ.ml  | 12 ++++++++----
 kernel/environ.mli |  2 +-
 2 files changed, 9 insertions(+), 5 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3