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 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'kernel/names.ml')

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