Merge branch 'v8.6'

4 files changed, 8 insertions, 8 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index c458894795..80b0b7e4c6 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -49,11 +49,11 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
 
 (** Shortcuts to make proof search easier. *)
 
-Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv.
+Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv | 1.
 
-Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.
+Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv | 1.
 
-Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
+Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1.
 
   Next Obligation.
   Proof. intros A R sa x y z Hxy Hyz.
@@ -123,7 +123,7 @@ Section Respecting.
 
 End Respecting.
 
-(** The default equivalence on function spaces, with higher-priority than [eq]. *)
+(** The default equivalence on function spaces, with higher priority than [eq]. *)
 
 Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) :
   Reflexive (pointwise_relation A eqB) | 9.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index a349eb9085..d6f9bb9df0 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -8,7 +8,6 @@
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
-Require Export ProofIrrelevance.
 Require Export JMeq.
 
 Require Import Coq.Program.Tactics.
@@ -143,7 +142,7 @@ Ltac pi_eq_proof_hyp p :=
       | [ H : X = Y |- _ ] =>
         match p with
           | H => fail 2
-          | _ => rewrite (proof_irrelevance (X = Y) p H)
+          | _ => rewrite (UIP _ X Y p H)
         end
       | _ => fail " No hypothesis with same type "
     end
@@ -166,7 +165,7 @@ Hint Rewrite <- eq_rect_eq : refl_id.
    [coerce_* t eq_refl = t]. *)
 
 Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl.
-Proof. apply proof_irrelevance. Qed.
+Proof. apply UIP. Qed.
 
 Lemma UIP_refl_refl A (x : A) :
   Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl.
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index c8f37318d1..2a3ec926b2 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -9,6 +9,7 @@
 
 Require Import Coq.Program.Utils.
 Require Import Coq.Program.Equality.
+Require Export ProofIrrelevance.
 
 Local Open Scope program_scope.
 
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v
index 10527442e8..d43baee8cd 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -339,7 +339,7 @@ Proof.
   rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0;
     rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5;
       rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5.
-  destruct (Rcase_abs x0) as [Hlt|Hgt]_eqn:Heqs.
+  destruct (Rcase_abs x0) as [Hlt|Hgt] eqn:Heqs.
   unfold sqrt. rewrite Heqs.
   rewrite Rabs_R0; apply H2.
   rewrite Rabs_right.