From afdb9b7fa4a6ce1165b270ffdae4574897aa7c40 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 1 Oct 2000 13:18:45 +0000
Subject: Déplacement 'a reference et binder_kind de Term vers Rawterm

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@619 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/rawterm.ml  | 9 +++++++++
 pretyping/rawterm.mli | 9 +++++++++
 2 files changed, 18 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index a3382f5cdf..294cbe320c 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -21,6 +21,15 @@ type cases_pattern =
 
 type rawsort = RProp of Term.contents | RType
 
+type binder_kind = BProd | BLambda | BLetIn
+
+type 'ctxt reference =
+  | RConst of section_path * 'ctxt
+  | RInd of inductive_path * 'ctxt
+  | RConstruct of constructor_path * 'ctxt
+  | RVar of identifier
+  | REVar of int * 'ctxt
+
 (*i Pas beau ce constr dans rawconstr, mais mal compris ce ctxt des ref i*)
 type rawconstr = 
   | RRef of loc * rawconstr array reference
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 5fb28fea03..4ee516b8b3 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -20,6 +20,15 @@ type cases_pattern =
 
 type rawsort = RProp of Term.contents | RType
 
+type binder_kind = BProd | BLambda | BLetIn
+
+type 'ctxt reference =
+  | RConst of section_path * 'ctxt
+  | RInd of inductive_path * 'ctxt
+  | RConstruct of constructor_path * 'ctxt
+  | RVar of identifier
+  | REVar of int * 'ctxt
+
 type rawconstr = 
   | RRef of loc * rawconstr array reference
   | RMeta of loc * int
-- 
cgit v1.2.3