Déplacement de global_reference dans Names pour pouvoir lier Nametab à grammar.cma

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 17 insertions, 20 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 811672ba3d..3aa20400a1 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -314,7 +314,8 @@ module Spset = Set.Make(SpOrdered)
 module Sppred = Predicate.Make(SpOrdered)
 module Spmap = Map.Make(SpOrdered)
 
-(* Special references for inductive objects *)
+(*s********************************************************************)
+(* type of global reference *)
 
 type variable = section_path
 type constant = section_path
@@ -322,6 +323,12 @@ type inductive = section_path * int
 type constructor = inductive * int
 type mutual_inductive = section_path
 
+type global_reference =
+  | VarRef of section_path
+  | ConstRef of constant
+  | IndRef of inductive
+  | ConstructRef of constructor
+
 (* Hash-consing of name objects *)
 module Hname = Hashcons.Make(
   struct 
diff --git a/kernel/names.mli b/kernel/names.mli
index cdf8c8c83a..a50dc28c4d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -111,13 +111,21 @@ module Spset  : Set.S with type elt = section_path
 module Sppred : Predicate.S with type elt = section_path
 module Spmap  : Map.S with type key = section_path
 
-(*s Specific paths for declarations *)
+(*s********************************************************************)
+(* type of global reference *)
+
 type variable = section_path
 type constant = section_path
 type inductive = section_path * int
 type constructor = inductive * int
 type mutual_inductive = section_path
 
+type global_reference =
+  | VarRef of section_path
+  | ConstRef of constant
+  | IndRef of inductive
+  | ConstructRef of constructor
+
 (* Hash-consing *)
 val hcons_names : unit ->
   (section_path -> section_path) * (section_path -> section_path) *
diff --git a/kernel/term.ml b/kernel/term.ml
index e79fd5fb36..ea720dbd38 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -58,15 +58,6 @@ let family_of_sort = function
   | Type _ -> InType
 
 (********************************************************************)
-(* type of global reference *)
-
-type global_reference =
-  | VarRef of section_path
-  | ConstRef of constant
-  | IndRef of inductive
-  | ConstructRef of constructor
-
-(********************************************************************)
 (*       Constructions as implemented                               *)
 (********************************************************************)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 248d572276..418ce22368 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -64,15 +64,6 @@ type ('constr, 'types) cofixpoint =
 end 
 
 (*s*******************************************************************)
-(* type of global reference *)
-
-type global_reference =
-  | VarRef of section_path
-  | ConstRef of constant
-  | IndRef of inductive
-  | ConstructRef of constructor
-
-(*s*******************************************************************)
 (* The type of constructions *)
 
 type constr