Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 24 insertions, 26 deletions

diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 4a3e4cd5..aa78fbda 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -1,21 +1,17 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reduction.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Term
 open Environ
 open Closure
-(*i*)
 
-(************************************************************************)
-(*s Reduction functions *)
+(***********************************************************************
+  s Reduction functions *)
 
 val whd_betaiotazeta        : constr -> constr
 val whd_betadeltaiota       : env -> constr -> constr
@@ -24,8 +20,8 @@ val whd_betadeltaiota_nolet : env -> constr -> constr
 val whd_betaiota      : constr -> constr
 val nf_betaiota      : constr -> constr
 
-(************************************************************************)
-(*s conversion functions *)
+(***********************************************************************
+  s conversion functions *)
 
 exception NotConvertible
 exception NotConvertibleVect of int
@@ -40,45 +36,47 @@ val sort_cmp :
 val conv_sort      : sorts conversion_function
 val conv_sort_leq  : sorts conversion_function
 
-val trans_conv_cmp       : conv_pb -> constr trans_conversion_function
+val trans_conv_cmp       : ?l2r:bool -> conv_pb -> constr trans_conversion_function
 val trans_conv           :
-  ?evars:(existential->constr option) -> constr trans_conversion_function
+  ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function
 val trans_conv_leq       :
-  ?evars:(existential->constr option) -> types trans_conversion_function
+  ?l2r:bool -> ?evars:(existential->constr option) -> types trans_conversion_function
 
-val conv_cmp       : conv_pb -> constr conversion_function
+val conv_cmp       : ?l2r:bool -> conv_pb -> constr conversion_function
 val conv           :
-  ?evars:(existential->constr option) -> constr conversion_function
+  ?l2r:bool -> ?evars:(existential->constr option) -> constr conversion_function
 val conv_leq       :
-  ?evars:(existential->constr option) -> types conversion_function
+  ?l2r:bool -> ?evars:(existential->constr option) -> types conversion_function
 val conv_leq_vecti :
-  ?evars:(existential->constr option) -> types array conversion_function
+  ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function
 
-(* option for conversion *)
+(** option for conversion *)
 val set_vm_conv : (conv_pb -> types conversion_function) -> unit
 val vm_conv : conv_pb -> types conversion_function
 
-val set_default_conv : (conv_pb -> types conversion_function) -> unit
-val default_conv     : conv_pb -> types conversion_function
-val default_conv_leq : types conversion_function
+val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit
+val default_conv     : conv_pb -> ?l2r:bool -> types conversion_function
+val default_conv_leq : ?l2r:bool -> types conversion_function
 
 (************************************************************************)
 
-(* Builds an application node, reducing beta redexes it may produce. *)
+(** Builds an application node, reducing beta redexes it may produce. *)
 val beta_appvect : constr -> constr array -> constr
 
-(* Builds an application node, reducing the [n] first beta-zeta redexes. *)
+(** Builds an application node, reducing the [n] first beta-zeta redexes. *)
 val betazeta_appvect : int -> constr -> constr array -> constr
 
-(* Pseudo-reduction rule  Prod(x,A,B) a --> B[x\a] *)
+(** Pseudo-reduction rule  Prod(x,A,B) a --> B[x\a] *)
 val hnf_prod_applist : env -> types -> constr list -> types
 
 
-(************************************************************************)
-(*s Recognizing products and arities modulo reduction *)
+(***********************************************************************
+  s Recognizing products and arities modulo reduction *)
 
 val dest_prod       : env -> types -> rel_context * types
 val dest_prod_assum : env -> types -> rel_context * types
 
-val dest_arity : env -> types -> arity
+exception NotArity
+
+val dest_arity : env -> types -> arity (* raises NotArity if not an arity *)
 val is_arity   : env -> types -> bool