diff options
Diffstat (limited to 'plugins/ring/LegacyZArithRing.v')
| -rw-r--r-- | plugins/ring/LegacyZArithRing.v | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v index d1412104..3f01a5c3 100644 --- a/plugins/ring/LegacyZArithRing.v +++ b/plugins/ring/LegacyZArithRing.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: LegacyZArithRing.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (* Instantiation of the Ring tactic for the binary integers of ZArith *) Require Export LegacyArithRing. @@ -15,7 +13,7 @@ Require Export ZArith_base. Require Import Eqdep_dec. Require Import LegacyRing. -Unboxed Definition Zeq (x y:Z) := +Definition Zeq (x y:Z) := match (x ?= y)%Z with | Datatypes.Eq => true | _ => false @@ -23,15 +21,15 @@ Unboxed Definition Zeq (x y:Z) := Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y. intros x y H; unfold Zeq in H. - apply Zcompare_Eq_eq. + apply Z.compare_eq. destruct (x ?= y)%Z; [ reflexivity | contradiction | contradiction ]. Qed. -Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq. +Definition ZTheory : Ring_Theory Z.add Z.mul 1%Z 0%Z Z.opp Zeq. split; intros; eauto with zarith. apply Zeq_prop; assumption. Qed. (* NatConstants and NatTheory are defined in Ring_theory.v *) -Add Legacy Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory +Add Legacy Ring Z Z.add Z.mul 1%Z 0%Z Z.opp Zeq ZTheory [ Zpos Zneg 0%Z xO xI 1%positive ]. |