diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-08-17 15:08:38 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-08-17 15:08:38 +0200 |
| commit | 02bcddbba985b65ac167f63b48bf2bd5bceffa1f (patch) | |
| tree | f71988937d028b2ff79476cf5235fe80ec617009 /theories/Classes | |
| parent | bc7ffd368789cb82bb8fc8b642b3de870b92c897 (diff) | |
Fix #4978: priorities of Equivalence instances
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/Equivalence.v | 8 |
1 files changed, 4 insertions, 4 deletions
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. |