From 20488fad20d360b834140eac4e7e97ab2e14f13b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 23 Feb 2004 16:02:36 +0000 Subject: [PATCH] bugfix in "elim ... using" tactical ("using" is a keyword) --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2