From 02bcddbba985b65ac167f63b48bf2bd5bceffa1f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 17 Aug 2016 15:08:38 +0200 Subject: Fix #4978: priorities of Equivalence instances --- theories/Classes/Equivalence.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'theories/Classes') diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index c45889479..80b0b7e4c 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. -- cgit v1.2.3