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/term.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'kernel/term.ml')

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