diff options
| author | Pierre-Marie Pédrot | 2018-11-19 19:34:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 19:34:42 +0100 |
| commit | 22c0b10f139d9a30fcbe4a5a489022e2b94130e9 (patch) | |
| tree | f4b84d2114aa4523aebf62f020ae46f4321fb10a /plugins/ssr | |
| parent | ba8e3caa31e464d1007c4ad54e8d70fd70ca3300 (diff) | |
| parent | eeb1d861551e25c6a92721334b3c9f36b7ebb012 (diff) | |
Merge PR #8987: Deprecate hint declaration/removal with no specified database
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrbool.v | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrfun.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index a618fc781f..3a7cf41d43 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -371,7 +371,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. -Hint Resolve is_true_true not_false_is_true is_true_locked_true. +Hint Resolve is_true_true not_false_is_true is_true_locked_true : core. (** Shorter names. **) Definition isT := is_true_true. diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index e2c0ed7c8b..6535cad8b7 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -398,7 +398,7 @@ End ExtensionalEquality. Typeclasses Opaque eqfun. Typeclasses Opaque eqrel. -Hint Resolve frefl rrefl. +Hint Resolve frefl rrefl : core. Notation "f1 =1 f2" := (eqfun f1 f2) (at level 70, no associativity) : fun_scope. |