diff options
Diffstat (limited to 'theories/Wellfounded')
| -rw-r--r-- | theories/Wellfounded/Inclusion.v | 1 | ||||
| -rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index 474836d53d..cafa849b1b 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -22,6 +22,7 @@ Section WfInclusion. apply Acc_intro; auto with sets. Qed. + #[local] Hint Resolve Acc_incl : core. Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index 2d139504f3..49c2dd8602 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -31,6 +31,7 @@ Section Wf_Transitive_Closure. apply Acc_inv with y; auto with sets. Defined. + #[local] Hint Resolve Acc_clos_trans : core. Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y. |