diff options
Diffstat (limited to 'kernel/reduction.mli')
-rw-r--r-- | kernel/reduction.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index ef764f34f..7db7e57bb 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -97,14 +97,19 @@ val default_conv_leq : ?l2r:bool -> types conversion_function (************************************************************************) (** Builds an application node, reducing beta redexes it may produce. *) +val beta_applist : constr -> constr list -> constr + +(** 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. *) -val betazeta_appvect : int -> constr -> constr array -> constr +(** Builds an application node, reducing beta redexe it may produce. *) +val beta_app : constr -> constr -> constr (** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types +(** Compatibility alias for Term.lambda_appvect_assum *) +val betazeta_appvect : int -> constr -> constr array -> constr (*********************************************************************** s Recognizing products and arities modulo reduction *) |