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/Wellfounded | |
| 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/Wellfounded')
| -rw-r--r-- | theories/Wellfounded/Inclusion.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index ff233ef9c6..18c4bedd9a 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -22,7 +22,7 @@ Section WfInclusion. apply Acc_intro; auto with sets. Qed. - Hint Resolve Acc_incl. + Hint Resolve Acc_incl : core. Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1. Proof. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index 59068623ae..0d56d88869 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -31,7 +31,7 @@ Section Wf_Transitive_Closure. apply Acc_inv with y; auto with sets. Defined. - Hint Resolve Acc_clos_trans. + Hint Resolve Acc_clos_trans : core. Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y. Proof. |