From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 13 Jul 2005 10:02:52 +0000 (+0000)
Subject: bugfix: "LPAREN" vs LPAREN
X-Git-Tag: pre_notation~23
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0a23b2111c404a0a7141a0d5729cf3aa0bdf7798;p=helm.git

bugfix: "LPAREN" vs LPAREN
---

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 01ed2906b..f4651d637 100644
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -362,7 +362,7 @@ EXTEND
           return_term loc (CicNotationUtil.boxify p)
       | "break" -> return_term loc (Layout Break)
 (*       | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *)
-      | "LPAREN"; p = l1_pattern; "RPAREN" ->
+      | LPAREN; p = l1_pattern; RPAREN ->
           return_term loc (CicNotationUtil.boxify p)
       ]
     | "simple" NONA