diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-16 16:30:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-16 16:30:21 +0000 |
| commit | 50cecafaef952ca0a6c2bf02c5d7d84e10e243fd (patch) | |
| tree | e0a1d4fdb31f37d10dba569ea1ac9c57f61320ed /parsing/g_constrnew.ml4 | |
| parent | 085ad75889659ab489fb3679e73a631df6d389ed (diff) | |
MAJ suppression 250
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5105 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_constrnew.ml4')
| -rw-r--r-- | parsing/g_constrnew.ml4 | 4 |
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)) ] ] ; |