From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 pretyping/rawterm.mli | 43 +++++++++++++++++++++++--------------------
 1 file changed, 23 insertions(+), 20 deletions(-)

(limited to 'pretyping/rawterm.mli')

diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 97e11af6..22317b5f 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,v 1.47.2.5 2005/01/21 16:42:37 herbelin Exp $ i*)
+(*i $Id: rawterm.mli 8624 2006-03-13 17:38:17Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -31,8 +31,6 @@ type patvar = identifier
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
-type fix_kind = RFix of (int array * int) | RCoFix of int
-
 type binder_kind = BProd | BLambda | BLetIn
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
@@ -46,14 +44,6 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
-type hole_kind =
-  | ImplicitArg of global_reference * (int * identifier option)
-  | BinderType of name
-  | QuestionMark
-  | CasesType
-  | InternalHole
-  | TomatchTypeParameter of inductive * int
-
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -63,26 +53,27 @@ type rawconstr =
   | RLambda of loc * name * rawconstr * rawconstr
   | RProd of loc * name * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * (rawconstr option * rawconstr option ref) *
-      (rawconstr * (name * (loc * inductive * name list) option) ref) list * 
+  | RCases of loc * rawconstr option *
+      (rawconstr * (name * (loc * inductive * name list) option)) list * 
       (loc * identifier list * cases_pattern list * rawconstr) list
-  | ROrderedCase of loc * case_style * rawconstr option * rawconstr * 
-      rawconstr array * rawconstr option ref
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
   | RRec of loc * fix_kind * identifier array * rawdecl list array *
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
-  | RHole of (loc * hole_kind)
-  | RCast of loc * rawconstr * rawconstr
+  | RHole of (loc * Evd.hole_kind)
+  | RCast of loc * rawconstr * cast_kind * rawconstr
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr
 
+and fix_recursion_order = RStructRec | RWfRec of rawconstr
+
+and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int
+
 val cases_predicate_names : 
-  (rawconstr * (name * (loc * inductive * name list) option) ref) list ->
-      name list
+  (rawconstr * (name * (loc * inductive * name list) option)) list -> 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
@@ -107,7 +98,18 @@ val occur_rawconstr : identifier -> rawconstr -> bool
 
 val loc_of_rawconstr : rawconstr -> loc
 
-val subst_raw : Names.substitution -> rawconstr -> rawconstr
+(**********************************************************************)
+(* Conversion from rawconstr to cases pattern, if possible            *)
+
+(* Take the current alias as parameter, raise Not_found if *)
+(* translation is impossible *)
+
+val cases_pattern_of_rawconstr : name -> rawconstr -> cases_pattern
+
+val rawconstr_of_closed_cases_pattern : cases_pattern -> name * rawconstr
+
+(**********************************************************************)
+(* Reduction expressions                                              *)
 
 type 'a raw_red_flag = {
   rBeta : bool;
@@ -131,6 +133,7 @@ type ('a,'b) red_expr_gen =
   | Fold of 'a list
   | Pattern of 'a occurrences list
   | ExtraRedExpr of string
+  | CbvVm
 
 type ('a,'b) may_eval =
   | ConstrTerm of 'a
-- 
cgit v1.2.3