From fa6f9f8441694f9af5dce403101fe6114876853c Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 21 Mar 2003 17:37:19 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Num/EqParams.v  |  4 ++--
 theories/Num/NSyntax.v   | 12 ++++++------
 theories/Num/NeqDef.v    |  2 +-
 theories/Num/NeqParams.v |  2 +-
 4 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'theories/Num')

diff --git a/theories/Num/EqParams.v b/theories/Num/EqParams.v
index f7fec9f92..c8fd74fcb 100644
--- a/theories/Num/EqParams.v
+++ b/theories/Num/EqParams.v
@@ -14,7 +14,7 @@ Require Export Params.
 
 Parameter eqN:N->N->Prop.  
 
-(*i Infix 6 "=" eqN. i*)
+(*i Infix 6 "=" eqN V8only 50. i*)
 
 Grammar constr constr1 :=
 eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
@@ -22,4 +22,4 @@ eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
 Syntax constr
   level 1:
     equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
-.
\ No newline at end of file
+.
diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v
index 7787c1f03..55912fdda 100644
--- a/theories/Num/NSyntax.v
+++ b/theories/Num/NSyntax.v
@@ -10,12 +10,12 @@
 
 Require Export Params.
 
-Infix 6 "<" lt.
-Infix 6 "<=" le.
-Infix 6 ">" gt.
-Infix 6 ">=" ge.
+Infix 6 "<" lt V8only 50.
+Infix 6 "<=" le V8only 50.
+Infix 6 ">" gt V8only 50.
+Infix 6 ">=" ge V8only 50.
 
-(*i Infix 7 "+" plus. i*)
+(*i Infix 7 "+" plus V8only 40. i*)
 
 Grammar constr lassoc_constr4 :=
   squash_sum
@@ -32,4 +32,4 @@ Grammar constr lassoc_constr4 :=
 Syntax constr
   level 4:
     sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
\ No newline at end of file
+.
diff --git a/theories/Num/NeqDef.v b/theories/Num/NeqDef.v
index 9d310a039..0e0029422 100644
--- a/theories/Num/NeqDef.v
+++ b/theories/Num/NeqDef.v
@@ -15,7 +15,7 @@ Require EqParams.
 Require EqAxioms.
 
 Definition neq : N -> N -> Prop := [x,y] ~(x=y).
-Infix 6 "<>" neq.
+Infix 6 "<>" neq V8only 50.
 
 (* Proofs of axioms *)
 Lemma eq_not_neq : (x,y:N)x=y->~(x<>y).
diff --git a/theories/Num/NeqParams.v b/theories/Num/NeqParams.v
index 4e651954f..7f7a5139e 100644
--- a/theories/Num/NeqParams.v
+++ b/theories/Num/NeqParams.v
@@ -15,7 +15,7 @@ Require Export Params.
 
 Parameter neq : N -> N -> Prop.
 
-Infix 6 "<>" neq.
+Infix 6 "<>" neq V8only 50.
 
 
 
-- 
cgit v1.2.3