Version initiale

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@134 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 13 deletions

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.mli
index 9ee7a02333..d30de0647b 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.mli
@@ -1,12 +1,13 @@
 open Names
 open CoqAst
 
-type constructor_id = ((section_path * int) * int) * identifier list
+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 * pattern list
-  | PatAs of loc * identifier * pattern;;
+  | 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
@@ -14,19 +15,21 @@ 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
+  | RInd of indtype_id * identifier list
+  | RConstruct of constructor_id * identifier list
   | RAbst of section_path
-  | RRel of int
-  | Var of identifier
-  | EVar of section_path * identifier list
+  | 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 * rawconstr option * rawconstr list * 
+  | RCases of loc * cases_style * rawconstr option * rawconstr list * 
       (identifier list * pattern list * rawconstr) list
   | ROldCase of loc * bool * rawconstr option * rawconstr * 
       rawconstr array
@@ -34,6 +37,7 @@ type rawconstr =
       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
@@ -42,8 +46,6 @@ type rawconstr =
   [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
+   - boolean in POldCase means it is recursive
    - option in PHole tell if the "?" was apparent or has been implicitely added
 *)
-
-