Merge branch 'v8.6'

5 files changed, 30 insertions, 18 deletions

diff --git a/test-suite/bugs/closed/3495.v b/test-suite/bugs/closed/3495.v
new file mode 100644
index 0000000000..102a2aba0d
--- /dev/null
+++ b/test-suite/bugs/closed/3495.v
@@ -0,0 +1,18 @@
+Require Import RelationClasses.
+
+Axiom R : Prop -> Prop -> Prop.
+Declare Instance : Reflexive R.
+
+Class bar := { x : False }.
+Record foo := { a : Prop ; b : bar }.
+
+Definition default_foo (a0 : Prop) `{b : bar} : foo := {| a := a0 ; b := b |}.
+
+Goal exists k, R k True.
+Proof.
+eexists.
+evar (b : bar).
+let e := match goal with |- R ?e _ => constr:(e) end in
+unify e (a (default_foo True)).
+subst b.
+reflexivity.
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 4ca6fe78cd..08628377f0 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -249,10 +249,10 @@ Section Reflective_Subuniverse.
  exact H.
     Defined.
 
-    Definition inO_paths@{i j} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : 
+    Definition inO_paths@{i} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : 
 S)    : In@{Ou Oa i} O (x=y).
     Proof.
-      simple refine (inO_to_O_retract@{i j} _ _ _); intro u.
+      simple refine (inO_to_O_retract@{i} _ _ _); intro u.
       -
  assert (p : (fun _ : O (x=y) => x) == (fun _=> y)).
         {
@@ -264,4 +264,4 @@ S)    : In@{Ou Oa i} O (x=y).
  hnf.
         rewrite O_indpaths_beta; reflexivity.
     Qed.
-    Check inO_paths@{Type Type}.
+    Check inO_paths@{Type}.
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index 048f31ce3d..da140c9318 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -652,7 +652,7 @@ Defined.
 
   Definition ReflectiveSubuniverse := Modality.
 
-  Definition O_reflector := O_reflector.
+  Definition O_reflector@{u a i} := O_reflector@{u a i}.
 
   Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
                    Type2le@{i a} -> Type2le@{i a}
@@ -660,7 +660,7 @@ Defined.
   Definition O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}),
                                In@{u a i} O (O_reflector@{u a i} O T)
     := O_inO@{u a i}.
-  Definition to := to.
+  Definition to@{u a i} := to@{u a i}.
   Definition inO_equiv_inO@{u a i j k} :
       forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j})
              (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f),
diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v
deleted file mode 100644
index ae8ed0e6e8..0000000000
--- a/test-suite/bugs/closed/4763.v
+++ /dev/null
@@ -1,13 +0,0 @@
-Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses.
-Coercion is_true : bool >-> Sortclass.
-Global Instance: Transitive leb.
-Admitted.
-
-Goal forall x y z, leb x y -> leb y z -> True.
-  intros ??? H H'.
-  lazymatch goal with
-  | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ]
-    => pose proof (transitivity H H' : is_true (R x z))
-  end.
-  exact I.
-Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/5097.v b/test-suite/bugs/closed/5097.v
new file mode 100644
index 0000000000..37b239cf61
--- /dev/null
+++ b/test-suite/bugs/closed/5097.v
@@ -0,0 +1,7 @@
+(* Tracing existing evars along the weakening rule ("clear") *)
+Goal forall y, exists x, x=0->x=y.
+intros.
+eexists ?[x].
+intros.
+let x:=constr:(ltac:(clear y; exact 0)) in idtac x.
+Abort.