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/ssr | |
| 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/ssr')
| -rw-r--r-- | theories/ssr/ssrbool.v | 1 | ||||
| -rw-r--r-- | theories/ssr/ssreflect.v | 2 | ||||
| -rw-r--r-- | theories/ssr/ssrfun.v | 1 |
3 files changed, 4 insertions, 0 deletions
diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index e8a036bbb0..b205965ed1 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -487,6 +487,7 @@ Ltac prop_congr := apply: prop_congr. Lemma is_true_true : true. Proof. by []. Qed. Lemma not_false_is_true : ~ false. Proof. by []. Qed. Lemma is_true_locked_true : locked true. Proof. by unlock. Qed. +#[global] Hint Resolve is_true_true not_false_is_true is_true_locked_true : core. (** Shorter names. **) diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v index 175cae8415..d0508bef2e 100644 --- a/theories/ssr/ssreflect.v +++ b/theories/ssr/ssreflect.v @@ -543,8 +543,10 @@ Proof. by move=> /(_ P); apply. Qed. Require Export ssrunder. +#[global] Hint Extern 0 (@Under_rel.Over_rel _ _ _ _) => solve [ apply: Under_rel.over_rel_done ] : core. +#[global] Hint Resolve Under_rel.over_rel_done : core. Register Under_rel.Under_rel as plugins.ssreflect.Under_rel. diff --git a/theories/ssr/ssrfun.v b/theories/ssr/ssrfun.v index 053e86dc34..e1442e1da2 100644 --- a/theories/ssr/ssrfun.v +++ b/theories/ssr/ssrfun.v @@ -450,6 +450,7 @@ End ExtensionalEquality. Typeclasses Opaque eqfun. Typeclasses Opaque eqrel. +#[global] Hint Resolve frefl rrefl : core. Notation "f1 =1 f2" := (eqfun f1 f2) : fun_scope. |