From ebc6741574ced219ad51e912b947c96e1d470772 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 21 Jan 2005 09:35:33 +0000 Subject: [PATCH] syntax changes: "." at the end of the phrase instead of ";;" --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 1b1d690bd..00b4c4418 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -344,7 +344,7 @@ EXTEND return_tactic loc (TacticAst.Transitivity t) ] ]; - tactical0: [ [ t = tactical; SYMBOL ";;" -> return_tactical loc t ] ]; + tactical0: [ [ t = tactical; SYMBOL "." -> return_tactical loc t ] ]; tactical: [ "command" NONA [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ] @@ -438,6 +438,10 @@ EXTEND return_command loc (TacticAst.Baseuri uri) | [ IDENT "check" | IDENT "Check" ]; t = term -> return_command loc (TacticAst.Check t) +(* + | [ IDENT "alias" | IDENT "Alias" ]; spec = alias_spec -> + return_command loc (TacticAst.Alias spec) +*) ] ]; script_entry: [ -- 2.39.2