diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 0e6a2b819..6f7e3f8f8 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -105,6 +105,12 @@ 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 +(** In [hnf_prod_applist_assum n c args], [c] is supposed to (whd-)reduce to + the form [∀Γ.t] with [Γ] of length [n] and possibly with let-ins; it + returns [t] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val hnf_prod_applist_assum : env -> int -> types -> constr list -> types + (** Compatibility alias for Term.lambda_appvect_assum *) val betazeta_appvect : int -> constr -> constr array -> constr |