diff options
| author | Pierre-Marie Pédrot | 2020-11-14 17:55:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-16 12:28:27 +0100 |
| commit | 68cd077344ce37db1a601079dbc4fdcae6c8d41f (patch) | |
| tree | edcad8a440c4fb61256ff26d5554dd17b8d03423 /theories/Classes/CRelationClasses.v | |
| parent | 7daf04e53bdee6b0c9d0171c1e0d05903d677d3a (diff) | |
Explicitly annotate all hint declarations of the standard library.
By default Coq stdlib warnings raise an error, so this is really required.
Diffstat (limited to 'theories/Classes/CRelationClasses.v')
| -rw-r--r-- | theories/Classes/CRelationClasses.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index 72a196ca7a..236d35b68e 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -203,22 +203,35 @@ Defined. (** Hints to drive the typeclass resolution avoiding loops due to the use of full unification. *) +#[global] Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances. +#[global] Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances. +#[global] Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances. +#[global] Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances. +#[global] Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances. +#[global] Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances. +#[global] Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances. +#[global] Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances. +#[global] Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances. +#[global] Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances. +#[global] Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances. +#[global] Hint Extern 4 (subrelation (flip _) _) => class_apply @subrelation_symmetric : typeclass_instances. +#[global] Hint Resolve irreflexivity : ord. Unset Implicit Arguments. @@ -231,6 +244,7 @@ Ltac solve_crelation := | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H end. +#[global] Hint Extern 4 => solve_crelation : crelations. (** We can already dualize all these properties. *) @@ -351,6 +365,7 @@ Section Binary. Qed. End Binary. +#[global] Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances. (** The partial order defined by subrelation and crelation equivalence. *) |