From 04ba8da34b0482df8cf67f9e6e820df873e1e13d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 19 Sep 2003 00:31:06 +0000
Subject: Section et report Infix hors section

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

diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index 165c26f148..55ccb93e6f 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -42,6 +42,8 @@ Bind Scope Z_scope with Z.
 Arguments Scope POS [ Z_scope ].
 Arguments Scope NEG [ Z_scope ].
 
+Section fast_integers.
+
 Inductive relation : Set := 
   EGAL :relation | INFERIEUR : relation | SUPERIEUR : relation.
 
@@ -1482,6 +1484,8 @@ Intros x y;Case x;Case y; [
   Simpl; Rewrite (ZC1 q p H); Trivial with arith].
 Qed.
 
+End fast_integers.
+
 V7only [
   Comments "Compatibility with the old version of times and times_convert".
   Syntactic Definition times1 :=
@@ -1489,3 +1493,9 @@ V7only [
   Syntactic Definition times1_convert :=
     [x,y:positive;_:positive->positive](times_convert x y).
 ].
+
+V8Infix "+" Zplus : Z_scope.
+V8Infix "*" times : positive_scope.
+V8Infix "+" Zplus : Z_scope.
+V8Infix "*" Zmult : Z_scope.
+V8Infix "?=" Zcompare (at level 50, no associativity) : Z_scope.
-- 
cgit v1.2.3