From ade8d5b089ee10d3f17cebcbc883cbc6c7343539 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Oct 2001 09:37:58 +0000
Subject: 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
---
 kernel/names.ml  |  9 ++++++++-
 kernel/names.mli | 10 +++++++++-
 kernel/term.ml   |  9 ---------
 kernel/term.mli  |  9 ---------
 4 files changed, 17 insertions(+), 20 deletions(-)

(limited to 'kernel')

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
@@ -57,15 +57,6 @@ let family_of_sort = function
   | Prop Pos -> InSet
   | 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
@@ -63,15 +63,6 @@ type ('constr, 'types) cofixpoint =
    de Bruijn indices. *)
 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 *)
 
-- 
cgit v1.2.3