From d2bd5d87d23d443f6e41496bdfe5f8e82d675634 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:59 +0000 Subject: Modularization of BinInt, related fixes in the stdlib All the functions about Z is now in a separated file BinIntDef, which is Included in BinInt.Z. This BinInt.Z directly implements ZAxiomsSig, and instantiates derived properties ZProp. Note that we refer to Z instead of t inside BinInt.Z, otherwise ring breaks later on @eq Z.t git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/setoid_ring/Field_theory.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/setoid_ring/Field_theory.v') diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 31372a001..766473c6f 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -835,7 +835,7 @@ destruct n. assert (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z. change ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z). - rewrite <- Zplus_assoc. rewrite (Zplus_assoc (- Zpos p4)). + rewrite <- Zplus_assoc. rewrite (Zplus_assoc (- Zpos p4)%Z). simpl. rewrite Pcompare_refl. simpl. reflexivity. unfold Zminus, Zopp in H0. simpl in H0. rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial. -- cgit v1.2.3