From 092c116f7b31a0ab9048502cd3afcd66a72541e8 Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 8 Dec 2003 19:36:10 +0000
Subject: correction bug: parentheses ne cassent plus les implicites on met la
 notation ( _ ) qu'autour des entiers positifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5078 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_constrnew.ml4 | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index eaaa0c5b2c..24294f90dd 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -195,7 +195,9 @@ GEXTEND Gram
       [ c=atomic_constr -> c
       | c=match_constr -> c
       | "("; c = operconstr; ")" ->
-          CNotation(loc,"( _ )",[c]) ] ]
+          (match c with
+              CNumeral(_,Bignat.POS _) -> CNotation(loc,"( _ )",[c])
+            | _ -> c) ] ]
   ;
   binder_constr:
     [ [ "forall"; bl = binder_list; ","; c = operconstr LEVEL "200" ->
-- 
cgit v1.2.3