diff options
| -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 |