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.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'kernel/reduction.ml') 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 = -- cgit v1.2.3