aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/seq.v
diff options
context:
space:
mode:
authorAnton Trunov2018-11-26 14:48:50 +0100
committerAnton Trunov2018-12-11 12:13:06 +0100
commit2e6e0001f8215e3c42f2557df42e0d6486035c07 (patch)
tree10e3129f0584233d7fb825973794b517371c6024 /mathcomp/ssreflect/seq.v
parent316cca94aef28c2023cd823c588b140e13d0aded (diff)
Fix some new warnings emitted by Coq 8.10:
``` Warning: Adding and removing hints in the core database implicitly is deprecated. Please specify a hint database. [implicit-core-hint-db,deprecated] ```
Diffstat (limited to 'mathcomp/ssreflect/seq.v')
-rw-r--r--mathcomp/ssreflect/seq.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index ba1f969..2c9fd64 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1422,7 +1422,7 @@ Qed.
Lemma perm_eq_refl s : perm_eq s s.
Proof. exact/perm_eqP. Qed.
-Hint Resolve perm_eq_refl.
+Hint Resolve perm_eq_refl : core.
Lemma perm_eq_sym : symmetric perm_eq.
Proof. by move=> s1 s2; apply/perm_eqP/perm_eqP=> ? ?. Qed.
@@ -1601,7 +1601,7 @@ Arguments perm_eqP {T s1 s2}.
Arguments perm_eqlP {T s1 s2}.
Arguments perm_eqrP {T s1 s2}.
Prenex Implicits perm_eq.
-Hint Resolve perm_eq_refl.
+Hint Resolve perm_eq_refl : core.
Section RotrLemmas.
@@ -1827,7 +1827,7 @@ Qed.
Lemma subseq_refl s : subseq s s.
Proof. by elim: s => //= x s IHs; rewrite eqxx. Qed.
-Hint Resolve subseq_refl.
+Hint Resolve subseq_refl : core.
Lemma cat_subseq s1 s2 s3 s4 :
subseq s1 s3 -> subseq s2 s4 -> subseq (s1 ++ s2) (s3 ++ s4).
@@ -1876,7 +1876,7 @@ End Subseq.
Prenex Implicits subseq.
Arguments subseqP {T s1 s2}.
-Hint Resolve subseq_refl.
+Hint Resolve subseq_refl : core.
Section Rem.