summaryrefslogtreecommitdiff
path: root/pretyping/reductionops.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /pretyping/reductionops.mli
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'pretyping/reductionops.mli')
-rw-r--r--pretyping/reductionops.mli17
1 files changed, 12 insertions, 5 deletions
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