diff options
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/CRelationClasses.v | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index ca38ac5b4..5e04671ba 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -341,13 +341,14 @@ Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : type (** The partial order defined by subrelation and crelation equivalence. *) -Program Instance subrelation_partial_order : - ! PartialOrder (crelation A) relation_equivalence subrelation. - -Next Obligation. -Proof. - unfold relation_equivalence in *. compute; firstorder. -Qed. +(* Program Instance subrelation_partial_order : *) +(* ! PartialOrder (crelation A) relation_equivalence subrelation. *) +(* Obligation Tactic := idtac. *) + +(* Next Obligation. *) +(* Proof. *) +(* intros x. refine (fun x => x). *) +(* Qed. *) Typeclasses Opaque relation_equivalence. |