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.
---
 test-suite/bugs/closed/bug_13581.v | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_13581.v

(limited to 'test-suite')

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


From 643c10a894c1db24dd8ab06cc4376c92ae8b7c3c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 4 Apr 2021 20:20:01 +0200
Subject: More extraction tests for inductive types with let-ins.

---
 test-suite/bugs/closed/bug_13581.v | 54 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_13581.v b/test-suite/bugs/closed/bug_13581.v
index 9f129f331e..910537cf11 100644
--- a/test-suite/bugs/closed/bug_13581.v
+++ b/test-suite/bugs/closed/bug_13581.v
@@ -4,3 +4,57 @@ 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.
+
+(* Extra tests *)
+
+Record R T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) := Build
+  { g : T0 -> let U:=T0 in U ; h : d = d ; x : nat ; y := x+x }.
+
+Definition r := {| g := (fun x : nat => x) ; h := eq_refl (eq_refl 0) ; x := 0 |}.
+
+Extraction TestCompile r.
+(*
+(** val r0 : nat r **)
+
+let r0 =
+  { g = (fun x0 -> x0); x = O }
+*)
+
+Inductive I T (a:T) (U:=T) (b:T) (c:=(a,b)) : forall d (e:=S d) (h : S d = e), Type :=
+| C : I T a b 0 eq_refl
+| D : J T a b true eq_refl -> I T a b 1 eq_refl
+with J T (a:T) (U:=T) (b:T) (c:=(a,b)) : forall (d:bool) (h:d = true), Type :=
+| E : I T a b 0 eq_refl -> J T a b true eq_refl.
+
+Definition c := D _ _ _ (E _ _ _ (C nat 0 0)).
+
+Extraction TestCompile c.
+
+(*
+(** val c : nat i **)
+
+let c =
+  D (E C)
+*)
+
+CoInductive V T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) :=
+  { k : T; b := c+e ; m : nat; z : option (W nat 0 0 eq_refl) }
+with W T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) :=
+  { l : V nat 0 0 eq_refl }.
+
+CoFixpoint v :=
+  {| k := 0 ; m := 0 ; z := Some w ; |}
+with w := {| l := v |}.
+
+Extraction TestCompile v.
+(*
+(** val v0 : nat v **)
+
+let rec v0 =
+  lazy (Build_V (O, O, (Some w0)))
+
+(** val w0 : nat w **)
+
+and w0 =
+  lazy (Build_W v0)
+*)
-- 
cgit v1.2.3