From ed9223cf5324aa3ae168e249de12ff663fc634af Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 20 Nov 2002 21:10:00 +0000
Subject: Les parenthèses de la notation '(n)' maintemant mises par ML pour un
 meilleur affichage des entiers dans le scope nat_scope

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3261 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_natsyntax.ml      |  4 +---
 theories/Init/PeanoSyntax.v | 28 ++++++++--------------------
 2 files changed, 9 insertions(+), 23 deletions(-)

diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index ae36762326..bf91dc37b8 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -81,11 +81,9 @@ let rec pr_external_S std_pr = function
 (* Prints not p, but the SUCCESSOR of p !!!!! *)
 let nat_printer std_pr p =
   match (int_of_nat p) with
-    | Some i -> str (string_of_int i)
+    | Some i -> str "(" ++ str (string_of_int i) ++ str ")"
     | None -> pr_S (pr_external_S std_pr p)
 
-let nat_printer_0 _ _ = str "0"
-
 let _ = Esyntax.Ppprim.add ("nat_printer", nat_printer)
 
 (* Declare the primitive parser *)
diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v
index f42fccfd90..cbf5c2d207 100644
--- a/theories/Init/PeanoSyntax.v
+++ b/theories/Init/PeanoSyntax.v
@@ -10,22 +10,10 @@
 Require Datatypes.
 Require Peano.
 
-(* This conflicts with expressions like "(0+x)" ...
-Grammar nat number :=.
-
-Grammar constr constr0 :=
-  natural_nat [ "(" nat:number($c) ")" ] -> [$c].
-
-Grammar constr pattern :=
-  natural_pat [ "(" nat:pat_number($c) ")" ] -> [$c].
-*)
-
 Syntax constr
-  level 10:
-  S [ (S $p) ] -> [$p:"nat_printer":9]
-| O [ O ] -> [ "0" ]
-.
-
+  level 0:
+    S [ (S $p) ] -> [$p:"nat_printer"]
+  | O [ O ]      -> ["(0)"].
 
 (* Outside the module to be able to parse the grammar for 0,1,2... !! *)
 Delimiters "'N:" nat_scope "'". (* "[N", "[N:", "]]" are conflicting *)
@@ -33,11 +21,11 @@ Delimiters "'N:" nat_scope "'". (* "[N", "[N:", "]]" are conflicting *)
 (* For parsing/printing based on scopes *)
 Module nat_scope.
 
-Infix 4 "+" plus : nat_scope.
-Infix 3 "*" mult : nat_scope.
-Infix NONA 5 "<=" le : nat_scope.
-Infix NONA 5 "<" lt : nat_scope.
-Infix NONA 5 ">=" ge : 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 ... " *) *)
 
 (* Warning: this hides sum and prod and breaks sumor symbolic notation *)
-- 
cgit v1.2.3