diff options
| -rw-r--r-- | parsing/g_constrnew.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
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" -> |