16 files changed, 202 insertions, 9 deletions

diff --git a/test-suite/bugs/closed/2141.v b/test-suite/bugs/closed/2141.v
index 098a7e9e72..c556ff0b2b 100644
--- a/test-suite/bugs/closed/2141.v
+++ b/test-suite/bugs/closed/2141.v
@@ -11,5 +11,6 @@ End FSetHide.
 
 Module NatSet' := FSetHide NatSet.
 Recursive Extraction NatSet'.fold.
+Extraction TestCompile NatSet'.fold.
 
 (* Extraction "test2141.ml" NatSet'.fold. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3287.v b/test-suite/bugs/closed/3287.v
index 1b758acd73..4b3e7ff054 100644
--- a/test-suite/bugs/closed/3287.v
+++ b/test-suite/bugs/closed/3287.v
@@ -6,6 +6,7 @@ Definition bar := true.
 End Foo.
 
 Recursive Extraction Foo.bar.
+Extraction TestCompile Foo.bar.
 
 Module Foo'.
 Definition foo := (I,I).
@@ -13,10 +14,6 @@ Definition bar := true.
 End Foo'.
 
 Recursive Extraction Foo'.bar.
+Extraction TestCompile Foo'.bar.
 
-Module Foo''.
-Definition foo := (I,I).
-Definition bar := true.
-End Foo''.
-
-Extraction Foo.bar.
+Extraction Foo'.bar.
diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v
index 2fb0a5439a..1d9488c6e1 100644
--- a/test-suite/bugs/closed/3923.v
+++ b/test-suite/bugs/closed/3923.v
@@ -33,3 +33,4 @@ Axiom empty_fieldstore : cert_fieldstore.
 End MkCertRuntimeTypes.
 
 Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *)
+Extraction TestCompile MkCertRuntimeTypes.
diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v
index a59975dbcf..d6660e3553 100644
--- a/test-suite/bugs/closed/4616.v
+++ b/test-suite/bugs/closed/4616.v
@@ -2,5 +2,6 @@ Require Coq.extraction.Extraction.
 
 Set Primitive Projections.
 Record Foo' := Foo { foo : Type }.
-Axiom f : forall t : Foo', foo t.
+Definition f := forall t : Foo', foo t.
 Extraction f.
+Extraction TestCompile f.
diff --git a/test-suite/bugs/closed/4709.v b/test-suite/bugs/closed/4709.v
new file mode 100644
index 0000000000..a9edcc8043
--- /dev/null
+++ b/test-suite/bugs/closed/4709.v
@@ -0,0 +1,18 @@
+
+(** Bug 4709 https://coq.inria.fr/bug/4709
+    Extraction wasn't reducing primitive projections in types. *)
+
+Require Extraction.
+
+Set Primitive Projections.
+
+Record t := Foo { foo : Type }.
+Definition ty := foo (Foo nat).
+
+(* Without proper reduction of primitive projections in
+   [extract_type], the type [ty] was extracted as [Tunknown].
+   Let's check it isn't the case anymore. *)
+
+Parameter check : nat.
+Extract Constant check => "(O:ty)".
+Extraction TestCompile ty check.
diff --git a/test-suite/bugs/closed/4710.v b/test-suite/bugs/closed/4710.v
index 5d8ca330ac..e792a36234 100644
--- a/test-suite/bugs/closed/4710.v
+++ b/test-suite/bugs/closed/4710.v
@@ -4,7 +4,6 @@ Set Primitive Projections.
 Record Foo' := Foo { foo : nat }.
 Extraction foo.
 Record Foo2 (a : nat) := Foo2c { foo2p : nat; foo2b : bool }.
-Extraction Language Ocaml.
 Extraction foo2p.
 
 Definition bla (x : Foo2 0) := foo2p _ x.
@@ -12,3 +11,5 @@ Extraction bla.
 
 Definition bla' (a : nat) (x : Foo2 a) := foo2b _ x.
 Extraction bla'.
+
+Extraction TestCompile foo foo2p bla bla'.
diff --git a/test-suite/bugs/closed/4720.v b/test-suite/bugs/closed/4720.v
new file mode 100644
index 0000000000..704331e784
--- /dev/null
+++ b/test-suite/bugs/closed/4720.v
@@ -0,0 +1,50 @@
+(** Bug 4720 : extraction and "with" in module type *)
+
+Module Type A.
+ Parameter t : Set.
+End A.
+
+Module A_instance <: A.
+ Definition t := nat.
+End A_instance.
+
+Module A_private : A.
+ Definition t := nat.
+End A_private.
+
+Module Type B.
+End B.
+
+Module Type C (b : B).
+ Declare Module a : A.
+End C.
+
+Module WithMod (a' : A) (b' : B) (c' : C b' with Module a := A_instance).
+End WithMod.
+
+Module WithDef (a' : A) (b' : B) (c' : C b' with Definition a.t := nat).
+End WithDef.
+
+Module WithModPriv (a' : A) (b' : B) (c' : C b' with Module a := A_private).
+End WithModPriv.
+
+(* The initial bug report was concerning the extraction of WithModPriv
+   in Coq 8.4, which was suboptimal: it was compiling, but could have been
+   turned into some faulty code since A_private and c'.a were not seen as
+   identical by the extraction.
+
+   In Coq 8.5 and 8.6, the extractions of WithMod, WithDef, WithModPriv
+   were all causing Anomaly or Assert Failure. This shoud be fixed now.
+*)
+
+Require Extraction.
+
+Recursive Extraction WithMod.
+
+Recursive Extraction WithDef.
+
+Recursive Extraction WithModPriv.
+
+(* Let's even check that all this extracted code is actually compilable: *)
+
+Extraction TestCompile WithMod WithDef WithModPriv.
diff --git a/test-suite/bugs/closed/4844.v b/test-suite/bugs/closed/4844.v
new file mode 100644
index 0000000000..f140939ccd
--- /dev/null
+++ b/test-suite/bugs/closed/4844.v
@@ -0,0 +1,47 @@
+
+(* Bug report 4844 (and 4824):
+   The Haskell extraction was erroneously considering [Any] and
+   [()] as convertible ([Tunknown] an [Tdummy] internally). *)
+
+(* A value with inner logical parts.
+   Its extracted type will be [Sum () ()]. *)
+
+Definition semilogic : True + True := inl I.
+
+(* Higher-order record, whose projection [ST] isn't expressible
+   as an Haskell (or OCaml) type. Hence [ST] is extracted as the
+   unknown type [Any] in Haskell. *)
+
+Record SomeType := { ST : Type }.
+
+Definition SomeTrue := {| ST := True |}.
+
+(* A first version of the issue:
+  [abstrSum] is extracted as [Sum Any Any], so an unsafeCoerce
+  is required to cast [semilogic] into [abstrSum SomeTrue]. *)
+
+Definition abstrSum (t : SomeType) := ((ST t) + (ST t))%type.
+
+Definition semilogic' : abstrSum SomeTrue := semilogic.
+
+(* A deeper version of the issue.
+   In the previous example, the extraction could have reduced
+   [abstrSum SomeTrue] into [True+True], solving the issue.
+   It might do so in future versions. But if we put an inductive
+   in the way, a reduction isn't helpful. *)
+
+Inductive box (t : SomeType) := Box : ST t + ST t -> box t.
+
+Definition boxed_semilogic : box SomeTrue :=
+ Box SomeTrue semilogic.
+
+Require Extraction.
+Extraction Language Haskell.
+Recursive Extraction semilogic' boxed_semilogic.
+(* Warning! To fully check that this bug is still closed,
+   you should run ghc on the extracted code:
+
+Extraction "bug4844.hs" semilogic' boxed_semilogic.
+ghc bug4844.hs
+
+*)
diff --git a/test-suite/bugs/closed/5177.v b/test-suite/bugs/closed/5177.v
new file mode 100644
index 0000000000..7c8af1e46e
--- /dev/null
+++ b/test-suite/bugs/closed/5177.v
@@ -0,0 +1,22 @@
+(* Bug 5177 https://coq.inria.fr/bug/5177 :
+   Extraction and module type containing application and "with" *)
+
+Module Type T.
+  Parameter t: Type.
+End T.
+
+Module Type A (MT: T).
+  Parameter t1: Type.
+  Parameter t2: Type.
+  Parameter bar: MT.t -> t1 -> t2.
+End A.
+
+Module MakeA(MT: T): A MT with Definition t1 := nat.
+  Definition t1 := nat.
+  Definition t2 := nat.
+  Definition bar (m: MT.t) (x:t1) := x.
+End MakeA.
+
+Require Extraction.
+Recursive Extraction MakeA.
+Extraction TestCompile MakeA.
diff --git a/test-suite/bugs/closed/5205.v b/test-suite/bugs/closed/5205.v
new file mode 100644
index 0000000000..406f37a4b1
--- /dev/null
+++ b/test-suite/bugs/closed/5205.v
@@ -0,0 +1,6 @@
+Definition foo (n : nat) (m : nat) : nat := m.
+
+Arguments foo {_} _, _ _.
+
+Check foo 1 1.
+Check foo (n:=1) 1.
diff --git a/test-suite/bugs/closed/5315.v b/test-suite/bugs/closed/5315.v
new file mode 100644
index 0000000000..f1f1b8c051
--- /dev/null
+++ b/test-suite/bugs/closed/5315.v
@@ -0,0 +1,10 @@
+Require Import Recdef.
+
+Function dumb_works (a:nat) {struct a} :=
+  match (fun x => x) a with O => O | S n' => dumb_works n' end.
+
+Function dumb_nope (a:nat) {struct a} :=
+  match (id (fun x => x)) a with O => O | S n' => dumb_nope n' end.
+
+(* This check is just present to ensure Function worked well *)
+Check R_dumb_nope_complete. 
\ No newline at end of file
diff --git a/test-suite/bugs/closed/5365.v b/test-suite/bugs/closed/5365.v
new file mode 100644
index 0000000000..be360d24d2
--- /dev/null
+++ b/test-suite/bugs/closed/5365.v
@@ -0,0 +1,13 @@
+
+Inductive TupleT : nat -> Type :=
+| nilT : TupleT 0
+| consT {n} A : (A -> TupleT n) -> TupleT (S n).
+
+Inductive Tuple : forall n, TupleT n -> Type :=
+  nil : Tuple _ nilT
+| cons {n A} (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F).
+
+Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type :=
+  tmNil : TupleMap _ nilT nilT
+| tmCons {n} {A B : Type} (F : A -> TupleT n) (G : B -> TupleT n)
+  : (forall x, sigT (fun y => TupleMap _ (F x) (G y))) -> TupleMap _ (consT A F) (consT B G).
diff --git a/test-suite/bugs/closed/5618.v b/test-suite/bugs/closed/5618.v
new file mode 100644
index 0000000000..ab88a88f44
--- /dev/null
+++ b/test-suite/bugs/closed/5618.v
@@ -0,0 +1,9 @@
+Require Import FunInd.
+
+Function test {T} (v : T) (x : nat) : nat :=
+  match x with
+  | 0 => 0
+  | S x' => test v x'
+  end.
+
+Check R_test_complete.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/5641.v b/test-suite/bugs/closed/5641.v
new file mode 100644
index 0000000000..9f3246f33d
--- /dev/null
+++ b/test-suite/bugs/closed/5641.v
@@ -0,0 +1,6 @@
+Set Universe Polymorphism.
+
+Definition foo@{i j} (A : Type@{i}) : Type@{j}.
+Proof.
+abstract (exact ltac:(abstract (exact A))).
+Defined.
diff --git a/test-suite/bugs/closed/5671.v b/test-suite/bugs/closed/5671.v
new file mode 100644
index 0000000000..c9a085045a
--- /dev/null
+++ b/test-suite/bugs/closed/5671.v
@@ -0,0 +1,7 @@
+(* Fixing Meta-unclean specialize *)
+
+Require Import Setoid.
+Axiom a : forall x, x=0 -> True.
+Lemma lem (x y1 y2:nat) (H:x=0) (H0:eq y1 y2) : y1 = y2.
+specialize a with (1:=H). clear H x. intros _.
+setoid_rewrite H0.
diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v
index cd9cad4064..7bed956f3e 100644
--- a/test-suite/bugs/closed/HoTT_coq_123.v
+++ b/test-suite/bugs/closed/HoTT_coq_123.v
@@ -104,11 +104,15 @@ Record Functor (C D : PreCategory) :=
     morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d)
   }.
 
+(** Workaround to simpl losing universe constraints, see bug #5645. *)
+Ltac simpl' :=
+  simpl; match goal with [ |- ?P ] => let T := type of P in idtac end.
+
 Global Instance trunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)}
 : IsTrunc n (forall a, P a) | 100.
 Proof.
     generalize dependent P.
-  induction n as [ | n' IH]; (simpl; intros P ?).
+  induction n as [ | n' IH]; (simpl'; intros P ?).
   - admit.
   - pose (fun f g => trunc_equiv (@apD10 A P f g) ^-1); admit.
 Defined.