From f0f5810c3947a9735a954de90efa43ac2739f2e8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 24 Nov 1999 14:50:54 +0000
Subject: Version initiale

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@134 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/rawterm.ml  | 49 -------------------------------------------------
 pretyping/rawterm.mli | 51 +++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 51 insertions(+), 49 deletions(-)
 delete mode 100644 pretyping/rawterm.ml
 create mode 100644 pretyping/rawterm.mli

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
deleted file mode 100644
index 9ee7a02333..0000000000
--- a/pretyping/rawterm.ml
+++ /dev/null
@@ -1,49 +0,0 @@
-open Names
-open CoqAst
-
-type constructor_id = ((section_path * int) * int) * identifier list
-
-type pattern =  (* locs here refers to the ident's location, not whole pat *)
-    PatVar of loc * name
-  | PatCstr of loc * constructor_id * pattern list
-  | PatAs of loc * identifier * pattern;;
-
-type binder_kind = BProd | BLambda
-type fix_kind = RFix of int array * int | RCofix of int
-type rawsort = RProp of Term.contents | RType
-
-type reference =
-  | RConst of section_path * identifier list
-  | Ind of section_path * int * identifier list
-  | Construct of constructor_id
-  | RAbst of section_path
-  | RRel of int
-  | Var of identifier
-  | EVar of section_path * identifier list
-  | RMeta of int
-
-type rawconstr = 
-  | RRef of loc * reference
-  | RApp of loc * rawconstr * rawconstr list
-  | RBinder of loc * binder_kind * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option * rawconstr list * 
-      (identifier list * pattern list * rawconstr) list
-  | ROldCase of loc * bool * rawconstr option * rawconstr * 
-      rawconstr array
-  | RRec of loc * fix_kind * identifier array * 
-      rawconstr array * rawconstr array
-  | RSort of loc * rawsort
-  | RHole of loc option
-
-(* - if PRec (_, names, arities, bodies) is in env then arities are
-   typed in env too and bodies are typed in env enriched by the
-   arities incrementally lifted 
-
-  [On pourrait plutot mettre les arités aves le type qu'elles auront
-   dans le contexte servant à typer les body ???]
-
-   - boolean in PApp means local turn off of implicit arg mode
-   - option in PHole tell if the "?" was apparent or has been implicitely added
-*)
-
-
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
new file mode 100644
index 0000000000..d30de0647b
--- /dev/null
+++ b/pretyping/rawterm.mli
@@ -0,0 +1,51 @@
+open Names
+open CoqAst
+
+type indtype_id = section_path * int
+type constructor_id = indtype_id * 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
+  | PatAs of loc * identifier * pattern
+
+type binder_kind = BProd | BLambda
+type fix_kind = RFix of int array * int | RCofix of int
+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
+  | RAbst of section_path
+  | RVar of identifier
+  | REVar of section_path * identifier list
+  | RMeta of int
+
+type cases_style = PrintLet | PrintIf | PrintCases
+
+type rawconstr = 
+  | RRef of loc * reference
+  | RRel of loc * int
+  | RApp of loc * rawconstr * rawconstr list
+  | RBinder of loc * binder_kind * name * rawconstr * rawconstr
+  | RCases of loc * cases_style * rawconstr option * rawconstr list * 
+      (identifier list * pattern list * rawconstr) list
+  | ROldCase of loc * bool * rawconstr option * rawconstr * 
+      rawconstr array
+  | RRec of loc * fix_kind * identifier array * 
+      rawconstr array * rawconstr array
+  | RSort of loc * rawsort
+  | RHole of loc option
+  | RCast of loc * rawconstr * rawconstr
+
+(* - if PRec (_, names, arities, bodies) is in env then arities are
+   typed in env too and bodies are typed in env enriched by the
+   arities incrementally lifted 
+
+  [On pourrait plutot mettre les arités aves le type qu'elles auront
+   dans le contexte servant à typer les body ???]
+
+   - boolean in POldCase means it is recursive
+   - option in PHole tell if the "?" was apparent or has been implicitely added
+*)
-- 
cgit v1.2.3