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/reductionops.mli | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

(limited to 'pretyping/reductionops.mli')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 65cdd5cd..ff55cc0e 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reductionops.mli,v 1.8.2.2 2004/07/16 19:30:46 herbelin Exp $ i*)
+(*i $Id: reductionops.mli 8708 2006-04-14 08:13:02Z jforest $ i*)
 
 (*i*)
 open Names
@@ -63,6 +63,7 @@ val nf_betaiota : local_reduction_function
 val nf_betadeltaiota : reduction_function
 val nf_evar : evar_map -> constr -> constr
 
+val nf_betaiotaevar_preserving_vm_cast : reduction_function
 (* Lazy strategy, weak head reduction *)
 val whd_evar :  evar_map -> constr -> constr
 val whd_beta : local_reduction_function
@@ -111,6 +112,10 @@ val whd_betadeltaiotaeta_stack :  stack_reduction_function
 val whd_betadeltaiotaeta_state :  state_reduction_function
 val whd_betadeltaiotaeta :  reduction_function
 
+
+
+
+
 val beta_applist : constr * constr list -> constr
 
 val hnf_prod_app     : env ->  evar_map -> constr -> constr -> constr
@@ -121,12 +126,14 @@ val hnf_lam_appvect  : env ->  evar_map -> constr -> constr array -> constr
 val hnf_lam_applist  : env ->  evar_map -> constr -> constr list -> constr
 
 val splay_prod : env ->  evar_map -> constr -> (name * constr) list * constr
+val splay_lambda : env ->  evar_map -> constr -> (name * constr) list * constr
 val splay_arity : env ->  evar_map -> constr -> (name * constr) list * sorts
 val sort_of_arity : env -> constr -> sorts
 val decomp_n_prod : 
   env ->  evar_map -> int -> constr -> Sign.rel_context * constr
 val splay_prod_assum :
   env ->  evar_map -> constr -> Sign.rel_context * constr
+val decomp_sort : env -> evar_map -> types -> sorts
 
 type 'a miota_args = {
   mP      : constr;     (* the result type *)
@@ -162,10 +169,6 @@ val reduce_fix : local_state_reduction_function -> fixpoint
 
 type conversion_test = constraints -> constraints
 
-type conv_pb = 
-  | CONV 
-  | CUMUL
-
 val pb_is_equal : conv_pb -> bool
 val pb_equal : conv_pb -> conv_pb
 
@@ -188,3 +191,7 @@ val instance : (metavariable * constr) list -> constr -> constr
 val hnf : env -> 'a evar_map -> constr -> constr * constr list
 i*)
 val apprec :  state_reduction_function
+
+(*s Meta-related reduction functions *)
+val meta_instance : evar_defs -> constr freelisted -> constr
+val nf_meta       : evar_defs -> constr -> constr
-- 
cgit v1.2.3