aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-16 16:30:21 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-16 16:30:21 +0000
commit50cecafaef952ca0a6c2bf02c5d7d84e10e243fd (patch)
treee0a1d4fdb31f37d10dba569ea1ac9c57f61320ed
parent085ad75889659ab489fb3679e73a631df6d389ed (diff)
MAJ suppression 250
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5105 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--parsing/g_constrnew.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 24294f90d..9320e5eb7 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -194,7 +194,7 @@ GEXTEND Gram
| "0"
[ c=atomic_constr -> c
| c=match_constr -> c
- | "("; c = operconstr; ")" ->
+ | "("; c = operconstr LEVEL "200"; ")" ->
(match c with
CNumeral(_,Bignat.POS _) -> CNotation(loc,"( _ )",[c])
| _ -> c) ] ]
@@ -303,7 +303,7 @@ GEXTEND Gram
| "0"
[ r = Prim.reference -> CPatAtom (loc,Some r)
| "_" -> CPatAtom (loc,None)
- | "("; p = pattern; ")" ->
+ | "("; p = pattern LEVEL "200"; ")" ->
CPatNotation(loc,"( _ )",[p])
| n = INT -> CPatNumeral (loc,Bignat.POS(Bignat.of_string n)) ] ]
;