Merge PR #1082: Fixing Print for inductive types with let-in in parameters

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