From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 pretyping/rawterm.mli | 32 ++++++++++++++++++++++----------
 1 file changed, 22 insertions(+), 10 deletions(-)

(limited to 'pretyping/rawterm.mli')

diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 546b36b0..2ba8022f 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rawterm.mli 9976 2007-07-12 11:58:30Z msozeau $ i*)
+(*i $Id: rawterm.mli 11094 2008-06-10 19:35:23Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -40,6 +40,8 @@ type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type binder_kind = BProd | BLambda | BLetIn
 
+type binding_kind = Explicit | Implicit
+
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
 
 type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list
@@ -61,10 +63,10 @@ type rawconstr =
   | REvar of loc * existential_key * rawconstr list option
   | RPatVar of loc * (bool * patvar) (* Used for patterns only *)
   | RApp of loc * rawconstr * rawconstr list
-  | RLambda of loc * name * rawconstr * rawconstr
-  | RProd of loc * name * rawconstr * rawconstr
+  | RLambda of loc * name * binding_kind *  rawconstr * rawconstr
+  | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses
+  | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
@@ -75,7 +77,7 @@ type rawconstr =
   | RCast of loc * rawconstr * rawconstr cast_type
   | RDynamic of loc * Dyn.t
 
-and rawdecl = name * rawconstr option * rawconstr
+and rawdecl = name * binding_kind * rawconstr option * rawconstr
 
 and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr
 
@@ -86,12 +88,15 @@ and fix_kind =
 and predicate_pattern =
     name * (loc * inductive * int * name list) option
 
-and tomatch_tuple = (rawconstr * predicate_pattern) list
+and tomatch_tuple = (rawconstr * predicate_pattern)
+
+and tomatch_tuples = tomatch_tuple list
+
+and cases_clause = (loc * identifier list * cases_pattern list * rawconstr)
 
-and cases_clauses =
-    (loc * identifier list * cases_pattern list * rawconstr) list
+and cases_clauses = cases_clause list
 
-val cases_predicate_names : tomatch_tuple -> name list
+val cases_predicate_names : tomatch_tuples -> name list
 
 (*i - if PRec (_, names, arities, bodies) is in env then arities are
    typed in env too and bodies are typed in env enriched by the
@@ -141,7 +146,14 @@ val all_flags : 'a raw_red_flag
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 
-type 'a with_occurrences = int or_var list * 'a
+type occurrences_expr = bool * int or_var list
+
+val all_occurrences_expr_but : int or_var list -> occurrences_expr
+val no_occurrences_expr_but : int or_var list -> occurrences_expr
+val all_occurrences_expr : occurrences_expr
+val no_occurrences_expr : occurrences_expr
+
+type 'a with_occurrences = occurrences_expr * 'a
 
 type ('a,'b) red_expr_gen =
   | Red of bool
-- 
cgit v1.2.3