From 8b882c1ab5a31eea35eec89f134238dd17b945c2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 30 Nov 1999 18:49:45 +0000
Subject: inductive_key et constructor_key

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@166 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/rawterm.mli | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index f2df08842d..03d0d6e47e 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -11,12 +11,12 @@ open Type_errors
 
 type loc = int * int
 
-type indtype_id = section_path * int
-type constructor_id = indtype_id * int
+type inductive_key = section_path * int
+type constructor_key = inductive_key * int
 
 type pattern =  (* locs here refers to the ident's location, not whole pat *)
   | PatVar of loc * name
-  | PatCstr of loc * (constructor_id * identifier list) * pattern list
+  | PatCstr of loc * (constructor_key * identifier list) * pattern list
   | PatAs of loc * identifier * pattern
 
 type binder_kind = BProd | BLambda
@@ -25,8 +25,8 @@ type rawsort = RProp of Term.contents | RType
 
 type reference =
   | RConst of section_path * identifier list
-  | RInd of indtype_id * identifier list
-  | RConstruct of constructor_id * identifier list
+  | RInd of inductive_key * identifier list
+  | RConstruct of constructor_key * identifier list
   | RAbst of section_path
   | RVar of identifier
   | REVar of int * identifier list
-- 
cgit v1.2.3