aboutsummaryrefslogtreecommitdiff
path: root/theories/Sorting/Permutation.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Sorting/Permutation.v')
-rw-r--r--theories/Sorting/Permutation.v1
1 files changed, 1 insertions, 0 deletions
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