Merge branch 'v8.5'

7 files changed, 74 insertions, 3 deletions

diff --git a/test-suite/bugs/closed/4378.v b/test-suite/bugs/closed/4378.v
new file mode 100644
index 000000000..9d5916556
--- /dev/null
+++ b/test-suite/bugs/closed/4378.v
@@ -0,0 +1,9 @@
+Tactic Notation "epose" open_constr(a) :=
+  let a' := fresh in
+  pose a as a'.
+Tactic Notation "epose2" open_constr(a) tactic3(tac) :=
+  let a' := fresh in
+  pose a as a'.
+Goal True.
+  epose _. Undo.
+  epose2 _ idtac.
diff --git a/test-suite/bugs/closed/4495.v b/test-suite/bugs/closed/4495.v
new file mode 100644
index 000000000..8b032db5f
--- /dev/null
+++ b/test-suite/bugs/closed/4495.v
@@ -0,0 +1 @@
+Fail Notation "'forall' x  ..  y ',' P " := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder).
diff --git a/test-suite/bugs/closed/4503.v b/test-suite/bugs/closed/4503.v
new file mode 100644
index 000000000..f54d6433d
--- /dev/null
+++ b/test-suite/bugs/closed/4503.v
@@ -0,0 +1,37 @@
+Require Coq.Classes.RelationClasses.
+
+Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
+{ refl : forall x, r x x }.
+
+(* FAILURE 1 *)
+
+Section foo.
+  Polymorphic Universes A.
+  Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
+
+  Fail Definition foo := PO.
+End foo.
+
+
+Module ILogic.
+
+Set Universe Polymorphism.
+
+(* Logical connectives *)
+Class ILogic@{L} (A : Type@{L}) : Type := mkILogic
+{
+  lentails: A -> A -> Prop;
+  lentailsPre:> RelationClasses.PreOrder lentails
+}.
+
+
+End ILogic.
+
+Set Printing Universes.
+
+(* There is stil a problem if the class is universe polymorphic *)
+Section Embed_ILogic_Pre.
+  Polymorphic Universes A T.
+  Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}.
+
+End Embed_ILogic_Pre.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4511.v b/test-suite/bugs/closed/4511.v
new file mode 100644
index 000000000..0cdb3aee4
--- /dev/null
+++ b/test-suite/bugs/closed/4511.v
@@ -0,0 +1,3 @@
+Goal True.
+Fail evar I.
+
diff --git a/test-suite/bugs/closed/4519.v b/test-suite/bugs/closed/4519.v
new file mode 100644
index 000000000..ccbc47d20
--- /dev/null
+++ b/test-suite/bugs/closed/4519.v
@@ -0,0 +1,21 @@
+Set Universe Polymorphism.
+Section foo.
+  Universe i.
+  Context (foo : Type@{i}) (bar : Type@{i}).
+  Definition qux@{i} (baz : Type@{i}) := foo -> bar.
+End foo.
+Set Printing Universes.
+Print qux. (* qux@{Top.42 Top.43} =
+fun foo bar _ : Type@{Top.42} => foo -> bar
+     : Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42}
+(* Top.42 Top.43 |=  *)
+(* This is wrong; the first two types are equal, but the last one is not *)
+
+qux is universe polymorphic
+Argument scopes are [type_scope type_scope type_scope]
+ *)
+Check qux nat nat nat : Set.
+Check qux nat nat Set : Set. (* Error:
+The term "qux@{Top.50 Top.51} ?T ?T0 Set" has type "Type@{Top.50}" while it is 
+expected to have type "Set"
+(universe inconsistency: Cannot enforce Top.50 = Set because Set < Top.50). *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/HoTT_coq_002.v b/test-suite/bugs/closed/HoTT_coq_002.v
index ba69f6b15..dba4d5998 100644
--- a/test-suite/bugs/closed/HoTT_coq_002.v
+++ b/test-suite/bugs/closed/HoTT_coq_002.v
@@ -9,7 +9,7 @@ Section SpecializedFunctor.
   (* Variable objC : Type. *)
   Context `(C : SpecializedCategory objC).
 
-  Polymorphic Record SpecializedFunctor := {
+  Record SpecializedFunctor := {
     ObjectOf' : objC -> Type;
     ObjectC : Object C
   }.
diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v
index 4938b80f9..008fb72c4 100644
--- a/test-suite/bugs/closed/HoTT_coq_020.v
+++ b/test-suite/bugs/closed/HoTT_coq_020.v
@@ -59,8 +59,8 @@ Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C
   := Build_Functor Cat0 C (fun x => match x with end).
 
 Section Law0.
-  Variable objC : Type.
-  Variable C : Category objC.
+  Polymorphic Variable objC : Type.
+  Polymorphic Variable C : Category objC.
 
   Set Printing All.
   Set Printing Universes.