From a265c1ad912b4940861ec27efd09e5b20d33233c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 6 Dec 2020 03:03:12 +0100
Subject: Fixing #13581: missing support for let-ins in arity of inductive
 types.

At first view, the fix takes care about when to use the number of
assumptions and when to also include local definitions, but I don't
know all the details of the implementation to be absolutely sure.
---
 plugins/extraction/extraction.ml   | 9 +++++----
 test-suite/bugs/closed/bug_13581.v | 6 ++++++
 2 files changed, 11 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_13581.v

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index ca4f5429a2..30f90dd1fc 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -427,6 +427,7 @@ and extract_really_ind env kn mib =
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
     let mip0 = mib.mind_packets.(0) in
+    let ndecls = List.length mib.mind_params_ctxt in
     let npar = mib.mind_nparams in
     let epar = push_rel_context mib.mind_params_ctxt env in
     let sg = Evd.from_env env in
@@ -462,17 +463,17 @@ and extract_really_ind env kn mib =
       if not p.ip_logical then
         let types = arities_of_constructors env ((kn,i),u) in
         for j = 0 to Array.length types - 1 do
-          let t = snd (decompose_prod_n npar types.(j)) in
+          let t = snd (decompose_prod_n_assum ndecls types.(j)) in
           let prods,head = dest_prod epar t in
           let nprods = List.length prods in
           let args = match Constr.kind head with
             | App (f,args) -> args (* [Constr.kind f = Ind ip] *)
             | _ -> [||]
           in
-          let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in
-          let db = db_from_ind dbmap npar in
+          let dbmap = parse_ind_args p.ip_sign args (nprods + ndecls) in
+          let db = db_from_ind dbmap ndecls in
           p.ip_types.(j) <-
-            extract_type_cons epar sg db dbmap (EConstr.of_constr t) (npar+1)
+            extract_type_cons epar sg db dbmap (EConstr.of_constr t) (ndecls+1)
         done
     done;
     (* Third pass: we determine special cases. *)
diff --git a/test-suite/bugs/closed/bug_13581.v b/test-suite/bugs/closed/bug_13581.v
new file mode 100644
index 0000000000..9f129f331e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13581.v
@@ -0,0 +1,6 @@
+From Coq Require Extraction.
+
+Record mixin_of T0 (b : unit) (T := T0) := Mixin { _ : T0 -> let U:=T0 in U }.
+Definition d := Mixin nat tt (fun x => x).
+
+Extraction TestCompile d.
-- 
cgit v1.2.3