From e0c06c7dac30b9959a3eb90b0c1d324f061a8660 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 00:46:41 +0100
Subject: Fixes incorrect anomaly message in lambda/prod_applist_assum + typo
 in doc.

Was introduced in e8c47b65.
---
 kernel/term.ml  | 6 ++++--
 kernel/term.mli | 4 ++--
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/kernel/term.ml b/kernel/term.ml
index aa88059524..ad1999f1cc 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 f5cb72f4e8..b0b5a15ac9 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
@@ -255,7 +255,7 @@ val prod_appvect : constr -> constr array -> constr
 val prod_applist : constr -> constr list -> constr
 
 (** 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
-- 
cgit v1.2.3


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 ++++++++++++
 kernel/reduction.mli            |  6 ++++++
 printing/printmod.ml            | 10 ++++++----
 test-suite/output/Inductive.out |  4 ++++
 test-suite/output/Inductive.v   |  4 ++++
 5 files changed, 32 insertions(+), 4 deletions(-)

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b0f4a1e5f1..7a4f25e633 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 =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 573e4c8bde..ce019f0216 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
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 05292b06ba..bed7c39fe6 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -93,10 +93,11 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
     else Univ.Instance.empty in
   let mip = mib.mind_packets.(i) in
   let params = Inductive.inductive_paramdecls (mib,u) in
+  let nparamdecls = Context.Rel.length params in
   let args = Context.Rel.to_extended_list mkRel 0 params in
-  let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
+  let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
-  let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
+  let cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls c args) cstrtypes in
   let envpar = push_rel_context params env in
   let inst =
     if Declareops.inductive_is_polymorphic mib then
@@ -174,10 +175,11 @@ let print_record env mind mib udecl =
   in
   let mip = mib.mind_packets.(0) in
   let params = Inductive.inductive_paramdecls (mib,u) in
+  let nparamdecls = Context.Rel.length params in
   let args = Context.Rel.to_extended_list mkRel 0 params in
-  let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
+  let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
-  let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
+  let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
   let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index e912003f03..af202ea01c 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,3 +1,7 @@
 The command has indeed failed with message:
 Last occurrence of "list'" must have "A" as 1st argument in
  "A -> list' A -> list' (A * A)%type".
+Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
+
+For foo: Argument scopes are [type_scope _]
+For Foo: Argument scopes are [type_scope _]
diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v
index 8db8956e32..8ff91268a6 100644
--- a/test-suite/output/Inductive.v
+++ b/test-suite/output/Inductive.v
@@ -1,3 +1,7 @@
 Fail Inductive list' (A:Set) : Set :=
 | nil' : list' A
 | cons' : A -> list' A -> list' (A*A).
+
+(* Check printing of let-ins *)
+Inductive foo (A : Type) (x : A) (y := x) := Foo.
+Print foo.
-- 
cgit v1.2.3


From c248228f5e910e19114e827661abb255c77a2b01 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 24 Sep 2017 10:27:03 +0200
Subject: Cosmetic: using "types" rather "constr" in some types of term.mli.

This enforces the intended meaning of the corresponding functions
(prod_appvect*/prod_applist*).
---
 kernel/term.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/kernel/term.mli b/kernel/term.mli
index b0b5a15ac9..a48d3de9ef 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -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 [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. } *)
 
-- 
cgit v1.2.3


From 42610a4659cf35e6a005d79eec273c606bdf87dd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 23 Sep 2017 12:46:35 +0200
Subject: Vm_compute: taking into account let-ins in parameters of
 constructors.

---
 pretyping/vnorm.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b5b8987e33..9cc635ed1d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -239,8 +239,9 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
       let (mib,mip) = Inductive.lookup_mind_specif env ind in
       let nparams = mib.mind_nparams in
       let params,realargs = Util.Array.chop nparams allargs in
+      let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
       let pT =
-	hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in
+        hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in
       let pT = whd_all env pT in
       let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
       (* Calcul du type des branches *)
-- 
cgit v1.2.3