From 63d582c6cd12bc3f8134a5aa9e3bdbca0dd2e9ca Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 23 Sep 2017 12:25:35 +0200 Subject: Fixing a bug of Print for inductive types with let-ins in parameters. Adding a "let-in"-sensitive function hnf_prod_applist_assum to instantiate parameters and using it for printing. Thanks to PMP for reporting. --- kernel/reduction.mli | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 573e4c8bd..ce019f021 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -103,6 +103,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 -- cgit v1.2.3