diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-02 12:04:04 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-02 12:04:04 -0700 |
| commit | c5f6e5947cd9a5a8daec65aeb065200f40f3f7a9 (patch) | |
| tree | fe1e282b957fe541873810cb02cb3238452bb37c /src/Algebra.v | |
| parent | 8453aea67d2c924d3ea51d5352e0b7a20588671a (diff) | |
Silence a warning about [Require] in 8.6
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index d23a13e1d..632eeac31 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -615,6 +615,7 @@ Module IntegralDomain. End IntegralDomain. End IntegralDomain. +Require Coq.setoid_ring.Field_theory. Module Field. Section Field. Context {T eq zero one opp add mul sub inv div} `{@field T eq zero one opp add sub mul inv div}. @@ -650,7 +651,6 @@ Module Field. + rewrite H1; apply left_identity. Qed. - Require Coq.setoid_ring.Field_theory. Lemma field_theory_for_stdlib_tactic : Field_theory.field_theory 0 1 add mul sub opp div inv eq. Proof. constructor. @@ -1350,8 +1350,9 @@ Section Example. Proof. intros. intro. nsatz_contradict. Qed. End Example. +Require Coq.ZArith.ZArith. Section Z. - Require Import ZArith. + Import ZArith. Global Instance ring_Z : @ring Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul. Proof. repeat split; auto using Z.eq_dec with zarith typeclass_instances. Qed. |