From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 20 Feb 2004 18:00:54 +0000 (+0000)
Subject: bugfix: "in" is an IDENT, not a keyword
X-Git-Tag: v0_0_4~124
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=54fa17c6db3db0b863cbfa6a0d4b7bf0d0641def;p=helm.git

bugfix: "in" is an IDENT, not a keyword
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index cd1de4487..efe959de8 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -203,7 +203,9 @@ EXTEND
       | PAREN "("; t = term; PAREN ")" -> return_term loc t
       ]
     ];
-  tactic_where: [ [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ] ];
+  tactic_where: [
+    [ where = OPT [ IDENT "in"; ident = IDENT -> ident ] -> where ]
+  ];
   tactic_term: [ [ t = term -> t ] ];
   ident_list0: [
     [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]