From 2ff1a8556490992e69743c954ce81e4c9da568f4 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 27 Oct 2003 18:12:21 +0000 Subject: Retour a un nommage non standard des variables pour compatibilite; report 'relation' pour compatibilite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4720 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/fast_integer.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v index 59ee28cd5..8563768bf 100644 --- a/theories/ZArith/fast_integer.v +++ b/theories/ZArith/fast_integer.v @@ -188,6 +188,7 @@ V8Infix "/" Zdiv2_pos : positive_scope. (**********************************************************************) (** Comparison on binary positive numbers *) +V7only [Notation relation := Datatypes.relation.]. Fixpoint compare [x,y:positive]: relation -> relation := [r:relation] @@ -2358,9 +2359,9 @@ Qed. (** Associativity mixed with commutativity *) -Theorem Zmult_permute : (x,y,z:Z)(Zmult x (Zmult y z)) = (Zmult y (Zmult x z)). +Theorem Zmult_permute : (n,m,p:Z)(Zmult n (Zmult m p)) = (Zmult m (Zmult n p)). Proof. -Intros; Rewrite -> (Zmult_assoc y x z); Rewrite -> (Zmult_sym y x). +Intros; Rewrite -> (Zmult_assoc m n p); Rewrite -> (Zmult_sym m n). Apply Zmult_assoc. Qed. -- cgit v1.2.3