diff options
| author | herbelin | 2002-12-07 17:27:55 +0000 |
|---|---|---|
| committer | herbelin | 2002-12-07 17:27:55 +0000 |
| commit | 0c3b7fd6677de61e435bbdbd89bcf3758396ef41 (patch) | |
| tree | 0bc83b3949ebae4ac04f19a83e5a8e540c833388 | |
| parent | 07f73dacfb68f36a366141d9545524d7afce4e9a (diff) | |
Compatibilité times1
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3387 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/ZArith/fast_integer.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v index 8f0b381ad0..59ea036255 100644 --- a/theories/ZArith/fast_integer.v +++ b/theories/ZArith/fast_integer.v @@ -1042,6 +1042,9 @@ Qed. Axiom times_convert : (x,y:positive) (convert x*y) = (mult (convert x) (convert y)). +Syntactic Definition times1 := times. +Syntactic Definition times1_convert := times_convert. + (** Multiplication on integers *) Definition Zmult := [x,y:Z] <Z>Cases x of |