diff options
| author | Maxime Dénès | 2018-11-13 16:39:54 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-14 08:53:03 +0100 |
| commit | eeb1d861551e25c6a92721334b3c9f36b7ebb012 (patch) | |
| tree | e51a9b33352681751c8eb67ca37fd8d4bd3033e1 /theories/Sets/Relations_3_facts.v | |
| parent | 94494770254bec236f2f6fe727ae42b79192afe4 (diff) | |
Deprecate hint declaration/removal with no specified database
Previously, hints added without a specified database where implicitly
put in the "core" database, which was discouraged by the user manual
(because of the lack of modularity of this approach).
Diffstat (limited to 'theories/Sets/Relations_3_facts.v')
| -rw-r--r-- | theories/Sets/Relations_3_facts.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index 0c1f670d0e..18ea019526 100644 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -38,7 +38,7 @@ Proof. intros U R x y H'; red. exists y; auto with sets. Qed. -Hint Resolve Rstar_imp_coherent. +Hint Resolve Rstar_imp_coherent : core. Theorem coherent_symmetric : forall (U:Type) (R:Relation U), Symmetric U (coherent U R). |