diff options
| author | coqbot-app[bot] | 2020-11-16 16:26:41 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-16 16:26:41 +0000 |
| commit | af96434d2991b9f01f6cd3963ed114b57e40792f (patch) | |
| tree | d10e879b4d7ae13c3623fd7073631e219f24753b /theories/Sorting | |
| parent | a400dbf104ea3bf0fef51a62e774fb4ff60a7397 (diff) | |
| parent | 4f28dd46d4bfce732693d6904f80e25b53d4fb2a (diff) | |
Merge PR #13384: Warn on hints without an explicit locality
Reviewed-by: Zimmi48
Diffstat (limited to 'theories/Sorting')
| -rw-r--r-- | theories/Sorting/CPermutation.v | 1 | ||||
| -rw-r--r-- | theories/Sorting/Heap.v | 2 | ||||
| -rw-r--r-- | theories/Sorting/Permutation.v | 1 | ||||
| -rw-r--r-- | theories/Sorting/Sorted.v | 2 |
4 files changed, 6 insertions, 0 deletions
diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v index 31d9f7f0ed..cebb0c808c 100644 --- a/theories/Sorting/CPermutation.v +++ b/theories/Sorting/CPermutation.v @@ -96,6 +96,7 @@ Qed. End CPermutation. +#[global] Hint Resolve CPermutation_refl : core. (* These hints do not reduce the size of the problem to solve and they diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 1130c9dd76..05a21620b7 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -36,7 +36,9 @@ Section defs. Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z. Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y. + #[local] Hint Resolve leA_refl : core. + #[local] Hint Immediate eqA_dec leA_dec leA_antisym : core. Let emptyBag := EmptyBag A. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 2f445c341a..45fb48ad5d 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -76,6 +76,7 @@ Qed. End Permutation. +#[global] Hint Resolve Permutation_refl perm_nil perm_skip : core. (* These hints do not reduce the size of the problem to solve and they diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 8cba461082..206eb606d2 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -137,7 +137,9 @@ Section defs. End defs. +#[global] Hint Constructors HdRel : core. +#[global] Hint Constructors Sorted : core. (* begin hide *) |