From d7a9fea94772971a52d04f9f266fe6d5e25cd40e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 2 May 2016 15:42:10 +0200
Subject: Avoid infinite loop/stack overflow when using "simpl nomatch" (bug
 #4576).

When encountering a "simpl nomatch" constant, the reduction machinery tries
to unfold it. If the subsequent partial reduction does not produce any
match construct, it keeps going from the reduced term. Unfortunately, the
reduced term has been refolded in the meantime, which means that some of
the previous reduction steps have been canceled, thus causing an infinite
loop. This patch delays the refolding till the very end, so that reduction
always progresses.

Disclaimer: I have no idea what I am doing here. The patch compiles the
standard library and the test suite properly, so hopefully they contain
enough tests to exercise the reduction machinery.
---
 test-suite/bugs/closed/4576.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/4576.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4576.v b/test-suite/bugs/closed/4576.v
new file mode 100644
index 0000000000..2c643ea779
--- /dev/null
+++ b/test-suite/bugs/closed/4576.v
@@ -0,0 +1,3 @@
+Definition foo := O.
+Arguments foo : simpl nomatch.
+Timeout 1 Eval cbn in id foo.
-- 
cgit v1.2.3


From 857e9ff0a7927d370c8a16e723385a9b199de872 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 2 May 2016 16:54:38 +0200
Subject: Properly handle notations containing spaces (bug #4538).

When a notation was starting or ending a space, Coq assumed the notation
had no terminal symbol in either places. Coq also considered a notation
containing only spaces to be productive. As stated in the documentation,
extraneous spaces are only meant as printing hints, they are not meant to
have any influence on parsing.
---
 test-suite/bugs/closed/4538.v | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 test-suite/bugs/closed/4538.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4538.v b/test-suite/bugs/closed/4538.v
new file mode 100644
index 0000000000..f925aae9e5
--- /dev/null
+++ b/test-suite/bugs/closed/4538.v
@@ -0,0 +1 @@
+Reserved Notation "   (u *)   ".
-- 
cgit v1.2.3


From f51dca0647b3213eb20a9b004372e5e6182bb29a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 May 2016 11:02:05 +0200
Subject: Call hooks when terminating a definition proof (bug #4663).

Also register properly the kind of definition.
---
 test-suite/bugs/closed/4663.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/4663.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4663.v b/test-suite/bugs/closed/4663.v
new file mode 100644
index 0000000000..b76619882a
--- /dev/null
+++ b/test-suite/bugs/closed/4663.v
@@ -0,0 +1,3 @@
+Coercion foo (n : nat) : Set.
+Admitted.
+Check (0 : Set).
-- 
cgit v1.2.3


From 443857fe1bbecf089eb40d522a71a014273c5a23 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 May 2016 14:06:17 +0200
Subject: Use the canonical name when looking for an eliminator (bug #4670).

Disclaimer: I have no idea what I am doing.
---
 test-suite/bugs/closed/4670.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/4670.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4670.v b/test-suite/bugs/closed/4670.v
new file mode 100644
index 0000000000..6113992953
--- /dev/null
+++ b/test-suite/bugs/closed/4670.v
@@ -0,0 +1,7 @@
+Require Import Coq.Vectors.Vector.
+Module Bar.
+  Definition foo A n (l : Vector.t A n) : True.
+  Proof.
+    induction l ; exact I.
+  Defined.
+End Bar.
-- 
cgit v1.2.3


From e7d54d7fe751e21001c6873fc6092b5adc8eb682 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 May 2016 14:22:04 +0200
Subject: Fix bug #4292: Unexpected functor objects.

---
 test-suite/bugs/closed/4292.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/4292.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4292.v b/test-suite/bugs/closed/4292.v
new file mode 100644
index 0000000000..403e155eaf
--- /dev/null
+++ b/test-suite/bugs/closed/4292.v
@@ -0,0 +1,7 @@
+Module Type S. End S.
+
+Declare Module M : S.
+
+Module Type F (T: S). End F.
+
+Fail Module Type N := F with Module T := M.
-- 
cgit v1.2.3


From 00a13c3c014e2729d17ad8e8191f20586ae3b52b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 3 May 2016 15:50:13 +0200
Subject: Test file for #4695: Slow Qed.

---
 test-suite/bugs/closed/4695.v | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 test-suite/bugs/closed/4695.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4695.v b/test-suite/bugs/closed/4695.v
new file mode 100644
index 0000000000..a42271811d
--- /dev/null
+++ b/test-suite/bugs/closed/4695.v
@@ -0,0 +1,38 @@
+(* 
+The Qed at the end of this file was slow in 8.5 and 8.5pl1 because the kernel
+term comparison after evaluation was done on constants according to their user
+names. The conversion still succeeded because delta applied, but was much
+slower than with a canonical names comparison.
+*)
+
+Module Mod0.
+
+  Fixpoint rec_ t d : nat :=
+    match d with
+    | O => O
+    | S d' =>
+      match t with
+      | true => rec_ t d'
+      | false => rec_ t d'
+      end
+    end.
+
+  Definition depth := 1000.
+
+  Definition rec t := rec_ t depth.
+
+End Mod0.
+
+
+Module Mod1.
+  Module M := Mod0.
+End Mod1.
+
+
+Axiom rec_prop : forall t d n, Mod1.M.rec_ t d = n.
+
+Lemma slow_qed : forall t n,
+    Mod0.rec t = n.
+Proof.
+  intros; unfold Mod0.rec; apply rec_prop.
+Timeout 2 Qed.
-- 
cgit v1.2.3


From b6e796a8ef956fa25bfeba84545f25b2cfb3aaf9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 May 2016 15:06:11 +0200
Subject: Fix bug #3825: Universe annotations on notations should pass through
 or be rejected.

---
 test-suite/bugs/closed/3825.v | 16 ++++++++++++++++
 test-suite/bugs/closed/3922.v |  2 +-
 test-suite/bugs/closed/4544.v |  2 +-
 3 files changed, 18 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/3825.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v
new file mode 100644
index 0000000000..e594b74b62
--- /dev/null
+++ b/test-suite/bugs/closed/3825.v
@@ -0,0 +1,16 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Axiom foo@{i j} : Type@{i} -> Type@{j}.
+
+Notation bar := foo.
+
+Monomorphic Universes i j.
+
+Check bar@{i j}.
+Fail Check bar@{i}.
+
+Notation qux := (nat -> nat).
+
+Fail Check qux@{i}.
+
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
index 5013bc6ac1..d88e8c3325 100644
--- a/test-suite/bugs/closed/3922.v
+++ b/test-suite/bugs/closed/3922.v
@@ -73,7 +73,7 @@ Definition Trunc_ind {n A}
   (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
   : (forall a, P (tr a)) -> (forall aa, P aa)
 := (fun f aa => match aa with tr a => fun _ => f a end Pt).
-Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+Definition merely (A : Type@{i}) : hProp := BuildhProp (Trunc -1 A).
 Definition cconst_factors_contr `{Funext}  {X Y : Type} (f : X -> Y)
            (P : Type) `{Pc : X -> Contr P}
            (g : X -> P) (h : P -> Y) (p : h o g == f)
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index d14cc86fc7..048f31ce3d 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -841,7 +841,7 @@ End Truncation_Modalities.
 
 Module Import TrM := Modalities_Theory Truncation_Modalities.
 
-Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+Definition merely (A : Type@{i}) : hProp := BuildhProp (Trunc -1 A).
 
 Notation IsSurjection := (IsConnMap -1).
 
-- 
cgit v1.2.3


From dd7cf3a8086fa8a08a421314caec8543ba62226b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 4 May 2016 10:36:43 +0200
Subject: Handle primitive projections inside types when extracting (bug
 #4616).

Note that extracting terms containing primitive projections is still
utterly broken, so don't use them.
---
 test-suite/bugs/closed/4616.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test-suite/bugs/closed/4616.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v
new file mode 100644
index 0000000000..c862f82067
--- /dev/null
+++ b/test-suite/bugs/closed/4616.v
@@ -0,0 +1,4 @@
+Set Primitive Projections.
+Record Foo' := Foo { foo : Type }.
+Axiom f : forall t : Foo', foo t.
+Extraction f.
-- 
cgit v1.2.3