Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 14 insertions, 21 deletions

diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index eecee8b0..b2b70bc9 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 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Util
@@ -46,7 +46,7 @@ type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
 
 type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list
 
-type 'a bindings = 
+type 'a bindings =
   | ImplicitBindings of 'a list
   | ExplicitBindings of 'a explicit_bindings
   | NoBindings
@@ -57,7 +57,7 @@ type 'a cast_type =
   | CastConv of cast_kind * 'a
   | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
 
-type rawconstr = 
+type rawconstr =
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
   | REvar of loc * existential_key * rawconstr list option
@@ -67,7 +67,7 @@ type rawconstr =
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
   | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
-  | RLetTuple of loc * name list * (name * rawconstr option) * 
+  | 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 *
@@ -79,7 +79,7 @@ type rawconstr =
 
 and rawdecl = name * binding_kind * rawconstr option * rawconstr
 
-and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr
+and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr * rawconstr option
 
 and fix_kind =
   | RFix of ((int option * fix_recursion_order) array * int)
@@ -98,21 +98,14 @@ and cases_clauses = cases_clause 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
-   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
-i*)
-
 val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr
 
+(** Ensure traversal from left to right *)
+val map_rawconstr_left_to_right :
+  (rawconstr -> rawconstr) -> rawconstr -> rawconstr
+
 (*i
-val map_rawconstr_with_binders_loc : loc -> 
+val map_rawconstr_with_binders_loc : loc ->
   (identifier -> 'a -> identifier * 'a) ->
   ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr
 i*)
@@ -155,10 +148,10 @@ val no_occurrences_expr : occurrences_expr
 
 type 'a with_occurrences = occurrences_expr * 'a
 
-type ('a,'b) red_expr_gen =
+type ('a,'b,'c) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl of 'a with_occurrences option
+  | Simpl of 'c with_occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
   | Unfold of 'b with_occurrences list
@@ -167,8 +160,8 @@ type ('a,'b) red_expr_gen =
   | ExtraRedExpr of string
   | CbvVm
 
-type ('a,'b) may_eval =
+type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a,'b) red_expr_gen * 'a
+  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a