8 files changed, 169 insertions, 13 deletions
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/4720.v b/test-suite/bugs/closed/4720.v
new file mode 100644
index 0000000000..9265b60c17
--- /dev/null
+++ b/test-suite/bugs/closed/4720.v
@@ -0,0 +1,46 @@
+(** 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.
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..231d103a59
--- /dev/null
+++ b/test-suite/bugs/closed/5177.v
@@ -0,0 +1,21 @@
+(* 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.
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/output/Notations3.out b/test-suite/output/Notations3.out
index ffea0819a5..a9ae74fd67 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -109,3 +109,9 @@ fun x : ?A => x === x
      : forall x : ?A, x = x
 where
 ?A : [x : ?A |- Type] (x cannot be used)
+{0, 1}
+     : nat * nat
+{0, 1, 2}
+     : nat * (nat * nat)
+{0, 1, 2, 3}
+     : nat * (nat * (nat * nat))
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 250aecafd4..dee0f70f79 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -160,3 +160,11 @@ End Bug4765.
 
 Notation "x === x" := (eq_refl x) (only printing, at level 10).
 Check (fun x => eq_refl x).
+
+(**********************************************************************)
+(* Test recursive notations with the recursive pattern repeated on the right *)
+
+Notation "{ x , .. , y , z }" := (pair x .. (pair y z) ..).
+Check {0,1}.
+Check {0,1,2}.
+Check {0,1,2,3}.
diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out
index 73369ab713..8b38fe0ff4 100644
--- a/test-suite/output/TypeclassDebug.out
+++ b/test-suite/output/TypeclassDebug.out
@@ -1,18 +1,18 @@
 Debug: 1: looking for foo without backtracking
 Debug: 1.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2 : foo
-Debug: 1.1-2: looking for foo without backtracking
-Debug: 1.1-2.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2.1-2 : foo
-Debug: 1.1-2.1-2: looking for foo without backtracking
-Debug: 1.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2.1-2.1-2 : foo
-Debug: 1.1-2.1-2.1-2: looking for foo without backtracking
-Debug: 1.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2.1-2.1-2.1-2 : foo
-Debug: 1.1-2.1-2.1-2.1-2: looking for foo without backtracking
-Debug: 1.1-2.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2.1-2.1-2.1-2.1-2 : foo
+Debug: 1.1-1 : foo
+Debug: 1.1-1: looking for foo without backtracking
+Debug: 1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1 : foo
+Debug: 1.1-1.1-1: looking for foo without backtracking
+Debug: 1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1.1-1 : foo
+Debug: 1.1-1.1-1.1-1: looking for foo without backtracking
+Debug: 1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1.1-1.1-1 : foo
+Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking
+Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo
 The command has indeed failed with message:
 Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed.
 Tactic failure: Proof search reached its limit.