diff options
| author | Anton Trunov | 2018-11-26 14:48:50 +0100 |
|---|---|---|
| committer | Anton Trunov | 2018-12-11 12:13:06 +0100 |
| commit | 2e6e0001f8215e3c42f2557df42e0d6486035c07 (patch) | |
| tree | 10e3129f0584233d7fb825973794b517371c6024 /mathcomp/algebra/interval.v | |
| parent | 316cca94aef28c2023cd823c588b140e13d0aded (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/algebra/interval.v')
| -rw-r--r-- | mathcomp/algebra/interval.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 1ca3414..b5d58cb 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -187,12 +187,12 @@ Proof. by move: bl br => [[] a|] [[] b|]. Qed. Lemma le_boundr_refl : reflexive le_boundr. Proof. by move=> [[] b|]; rewrite /le_boundr /= ?lerr. Qed. -Hint Resolve le_boundr_refl. +Hint Resolve le_boundr_refl : core. Lemma le_boundl_refl : reflexive le_boundl. Proof. by move=> [[] b|]; rewrite /le_boundl /= ?lerr. Qed. -Hint Resolve le_boundl_refl. +Hint Resolve le_boundl_refl : core. Lemma le_boundl_bb x b1 b2 : le_boundl (BOpen_if b1 x) (BOpen_if b2 x) = (b1 ==> b2). @@ -242,7 +242,7 @@ move=> x [[[] a|] [[] b|]]; move/itv_dec=> //= [hl hu]; do ?[split=> //; | by apply: negbTE; rewrite ltr_geF // (@ler_lt_trans _ x)]. Qed. -Hint Rewrite intP. +Hint Rewrite intP : core. Arguments itvP [x i]. Definition subitv (i1 i2 : interval R) := |