From 356c712e811c23e496ace3684b3345972b5d8f71 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 15 Dec 2002 12:32:15 +0000
Subject: Ajout syntaxe '>'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3444 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/PeanoSyntax.v | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v
index adb917b765..de3bac0d8e 100644
--- a/theories/Init/PeanoSyntax.v
+++ b/theories/Init/PeanoSyntax.v
@@ -21,20 +21,21 @@ Delimits Scope nat_scope with N.
 (* For parsing/printing based on scopes *)
 Module nat_scope.
 
-Infix LEFTA 4 "+" plus : nat_scope.
-Infix LEFTA 3 "*" mult : nat_scope.
-Infix 5 "<=" le : nat_scope.
-Infix 5 "<" lt : nat_scope.
-Infix 5 ">=" ge : nat_scope.
-(* Infix 5 ">" gt : nat_scope. (* Conflicts with "<..>Cases ... " *) *)
+Infix "+" plus (at level 4) : nat_scope.
+Infix "*" mult (at level 3): nat_scope.
+Infix "<=" le (at level 5, no associativity) : nat_scope.
+Infix "<" lt (at level 5, no associativity) : nat_scope.
+Infix ">=" ge (at level 5, no associativity) : nat_scope.
+Infix ">" gt (at level 5, no associativity) : nat_scope.
 
 (* Warning: this hides sum and prod and breaks sumor symbolic notation *)
 Open Scope nat_scope.
 
+(*
 Syntax constr
   level 0:
   S' [ (S $p) ] -> [$p:"nat_printer_S":9]
 | O' [ O ] -> [ _:"nat_printer_O" ]
 .
-
+*)
 End nat_scope.
-- 
cgit v1.2.3