From 24b229fdaf8d2c2516be55296c965831ded46c5c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Dec 2002 10:33:52 +0000
Subject: Compatibilite times1 (suite)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3415 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/fast_integer.v | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index 210e0846ba..fe16e8dff4 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).
+].
-- 
cgit v1.2.3