diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-27 18:12:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-27 18:12:21 +0000 |
| commit | 2ff1a8556490992e69743c954ce81e4c9da568f4 (patch) | |
| tree | a3d866a109cfd1d2f1af0b44094c0dc6f9009372 | |
| parent | 1d6edcfa1b5969f082572d2b083b8160c2385bcd (diff) | |
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
| -rw-r--r-- | theories/ZArith/fast_integer.v | 5 |
1 files 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. |