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/algebra/rat.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/algebra/rat.v')
| -rw-r--r-- | mathcomp/algebra/rat.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 6015f33..14fde5a 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -56,7 +56,7 @@ Definition denq x := nosimpl ((valq x).2). Lemma denq_gt0 x : 0 < denq x. Proof. by rewrite /denq; case: x=> [[a b] /= /andP []]. Qed. -Hint Resolve denq_gt0. +Hint Resolve denq_gt0 : core. Definition denq_ge0 x := ltrW (denq_gt0 x). @@ -64,7 +64,7 @@ Lemma denq_lt0 x : (denq x < 0) = false. Proof. by rewrite ltr_gtF. Qed. Lemma denq_neq0 x : denq x != 0. Proof. by rewrite /denq gtr_eqF ?denq_gt0. Qed. -Hint Resolve denq_neq0. +Hint Resolve denq_neq0 : core. Lemma denq_eq0 x : (denq x == 0) = false. Proof. exact: negPf (denq_neq0 _). Qed. @@ -368,7 +368,7 @@ Qed. Notation "n %:Q" := ((n : int)%:~R : rat) (at level 2, left associativity, format "n %:Q") : ring_scope. -Hint Resolve denq_neq0 denq_gt0 denq_ge0. +Hint Resolve denq_neq0 denq_gt0 denq_ge0 : core. Definition subq (x y : rat) : rat := (addq x (oppq y)). Definition divq (x y : rat) : rat := (mulq x (invq y)). |