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.

1 files changed, 12 insertions, 0 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b0f4a1e5f..7a4f25e63 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -938,6 +938,18 @@ let hnf_prod_app env t n =
 let hnf_prod_applist env t nl =
   List.fold_left (hnf_prod_app env) t nl
 
+let hnf_prod_applist_assum env n c l =
+  let rec app n subst t l =
+    if Int.equal n 0 then
+      if l == [] then substl subst t
+      else anomaly (Pp.str "Too many arguments.")
+    else match kind (whd_allnolet env t), l with
+    | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l
+    | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+    | _, [] -> anomaly (Pp.str "Not enough arguments.")
+    | _ -> anomaly (Pp.str "Not enough prod/let's.") in
+  app n [] c l
+
 (* Dealing with arities *)
 
 let dest_prod env =