diff options
| author | Cyril Cohen | 2018-12-11 13:36:32 +0100 |
|---|---|---|
| committer | GitHub | 2018-12-11 13:36:32 +0100 |
| commit | b2d25dc356c4a2500d861e7d3eb5a272a3072129 (patch) | |
| tree | 10e3129f0584233d7fb825973794b517371c6024 /mathcomp/ssreflect/seq.v | |
| parent | 316cca94aef28c2023cd823c588b140e13d0aded (diff) | |
| parent | 2e6e0001f8215e3c42f2557df42e0d6486035c07 (diff) | |
Merge pull request #252 from anton-trunov/implicit-core-hint-db
Fix some new warnings emitted by Coq 8.10
Diffstat (limited to 'mathcomp/ssreflect/seq.v')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 8 |
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. |