From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 23 Feb 2004 16:02:36 +0000 (+0000)
Subject: bugfix in "elim ... using" tactical ("using" is a keyword)
X-Git-Tag: v0_0_4~103
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=20488fad20d360b834140eac4e7e97ab2e14f13b;p=helm.git

bugfix in "elim ... using" tactical ("using" is a keyword)
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 26fc36c78..7c0dfc1c6 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -235,7 +235,7 @@ EXTEND
     | IDENT "elim"; IDENT "type"; t = tactic_term ->
         return_tactic loc (TacticAst.ElimType t)
     | IDENT "elim"; t1 = tactic_term;
-      using = OPT [ IDENT "using"; using = tactic_term -> using ] ->
+      using = OPT [ "using"; using = tactic_term -> using ] ->
         return_tactic loc (TacticAst.Elim (t1, using))
     | IDENT "exact"; t = tactic_term -> return_tactic loc (TacticAst.Exact t)
     | IDENT "exists" -> return_tactic loc TacticAst.Exists