diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-10 10:33:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-10 10:33:52 +0000 |
| commit | 24b229fdaf8d2c2516be55296c965831ded46c5c (patch) | |
| tree | 38c0721ae1d03ecf276496fbb44f5529cb738531 | |
| parent | e17714e8d8b35202537098605f4b2226caae3147 (diff) | |
Compatibilite times1 (suite)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3415 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/ZArith/fast_integer.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v index 210e0846b..fe16e8dff 100644 --- a/theories/ZArith/fast_integer.v +++ b/theories/ZArith/fast_integer.v @@ -1481,5 +1481,10 @@ Intros x y;Case x;Case y; [ Qed. End fast_integers. -Syntactic Definition times1 := times. -Syntactic Definition times1_convert := times_convert. +V7only [ + Comments "Compatibility with the old version of times and times_convert". + Syntactic Definition times1 := + [x:positive;_:positive->positive;y:positive](times x y). + Syntactic Definition times1_convert := + [x,y:positive;_:positive->positive](times_convert x y). +]. |