diff options
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/RelationClasses.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index dcf3139b2..80592d136 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -69,15 +69,15 @@ Program Instance flip_Irreflexive [ Irreflexive A R ] : Irreflexive (flip R) := Program Instance flip_Symmetric [ Symmetric A R ] : Symmetric (flip R). - Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric. + Solve Obligations using unfold flip ; program_simpl ; typeclass_app Symmetric. Program Instance flip_Asymmetric [ Asymmetric A R ] : Asymmetric (flip R). - Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry. + Solve Obligations using program_simpl ; unfold flip in * ; intros ; typeclass_app asymmetry ; eauto. Program Instance flip_Transitive [ Transitive A R ] : Transitive (flip R). - Solve Obligations using unfold flip ; program_simpl ; clapply transitivity. + Solve Obligations using unfold flip ; program_simpl ; typeclass_app transitivity ; eauto. Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A) ] : Irreflexive (complement R). @@ -390,3 +390,6 @@ Program Instance subrelation_partial_order : Proof. unfold relation_equivalence in *. firstorder. Qed. + +Typeclasses Opaque arrows predicate_implication predicate_equivalence + relation_equivalence. |