Merge branch 'v8.5'

10 files changed, 81 insertions, 2 deletions

diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v
new file mode 100644
index 000000000..e594b74b6
--- /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 5013bc6ac..d88e8c332 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/4292.v b/test-suite/bugs/closed/4292.v
new file mode 100644
index 000000000..403e155ea
--- /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.
diff --git a/test-suite/bugs/closed/4538.v b/test-suite/bugs/closed/4538.v
new file mode 100644
index 000000000..f925aae9e
--- /dev/null
+++ b/test-suite/bugs/closed/4538.v
@@ -0,0 +1 @@
+Reserved Notation "   (u *)   ".
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index d14cc86fc..048f31ce3 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).
 
diff --git a/test-suite/bugs/closed/4576.v b/test-suite/bugs/closed/4576.v
new file mode 100644
index 000000000..2c643ea77
--- /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.
diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v
new file mode 100644
index 000000000..c862f8206
--- /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.
diff --git a/test-suite/bugs/closed/4663.v b/test-suite/bugs/closed/4663.v
new file mode 100644
index 000000000..b76619882
--- /dev/null
+++ b/test-suite/bugs/closed/4663.v
@@ -0,0 +1,3 @@
+Coercion foo (n : nat) : Set.
+Admitted.
+Check (0 : Set).
diff --git a/test-suite/bugs/closed/4670.v b/test-suite/bugs/closed/4670.v
new file mode 100644
index 000000000..611399295
--- /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.
diff --git a/test-suite/bugs/closed/4695.v b/test-suite/bugs/closed/4695.v
new file mode 100644
index 000000000..a42271811
--- /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.