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

4 files changed, 28 insertions, 8 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 159d2ea66..da7042713 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -882,6 +882,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 =
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
 
diff --git a/kernel/term.ml b/kernel/term.ml
index fae990d45..a4c92bd33 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -352,10 +352,11 @@ let lambda_applist_assum 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 "Not enough arguments.")
+      else anomaly (Pp.str "Too many arguments.")
     else match kind_of_term t, l with
     | Lambda(_,_,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 lambda/let's.") in
   app n [] c l
 
@@ -377,10 +378,11 @@ let prod_applist_assum 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 "Not enough arguments.")
+      else anomaly (Pp.str "Too many arguments.")
     else match kind_of_term 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
 
diff --git a/kernel/term.mli b/kernel/term.mli
index c9a8cf6e1..b4597676a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -242,7 +242,7 @@ val lambda_applist : constr -> constr list -> constr
 val lambda_appvect : constr -> constr array -> constr
 
 (** In [lambda_applist_assum n c args], [c] is supposed to have the
-    form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it
+    form [λΓ.c] with [Γ] of length [n] and possibly with let-ins; it
     returns [c] with the assumptions of [Γ] instantiated by [args] and
     the local definitions of [Γ] expanded. *)
 val lambda_applist_assum : int -> constr -> constr list -> constr
@@ -251,15 +251,15 @@ val lambda_appvect_assum : int -> constr -> constr array -> constr
 (** pseudo-reduction rule *)
 
 (** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *)
-val prod_appvect : constr -> constr array -> constr
-val prod_applist : constr -> constr list -> constr
+val prod_appvect : types -> constr array -> types
+val prod_applist : types -> constr list -> types
 
 (** In [prod_appvect_assum n c args], [c] is supposed to have the
-    form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it
+    form [∀Γ.c] with [Γ] of length [n] and possibly with let-ins; it
     returns [c] with the assumptions of [Γ] instantiated by [args] and
     the local definitions of [Γ] expanded. *)
-val prod_appvect_assum : int -> constr -> constr array -> constr
-val prod_applist_assum : int -> constr -> constr list -> constr
+val prod_appvect_assum : int -> types -> constr array -> types
+val prod_applist_assum : int -> types -> constr list -> types
 
 (** {5 Other term destructors. } *)