From bc399fb172ecd3b598844a99eefb817ee0675e3d Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 10 Nov 2004 12:02:21 +0000 Subject: [PATCH] parse Baseuri command --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 53559bcd2..775f13f7d 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -314,7 +314,7 @@ EXTEND return_tactic loc (TacticAst.Transitivity t) ] ]; - tactical0: [ [ t = tactical; SYMBOL ";;" -> t ] ]; + tactical0: [ [ t = tactical; SYMBOL ";;" -> return_tactical loc t ] ]; tactical: [ "command" NONA [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ] @@ -371,6 +371,8 @@ EXTEND return_command loc (TacticAst.Undo (int_opt steps)) | [ IDENT "redo" | IDENT "Redo" ]; steps = OPT NUM -> return_command loc (TacticAst.Redo (int_opt steps)) + | [ IDENT "baseuri" | IDENT "Baseuri" ]; uri = OPT QSTRING -> + return_command loc (TacticAst.Baseuri uri) | [ IDENT "check" | IDENT "Check" ]; t = term -> return_command loc (TacticAst.Check t) ] -- 2.39.2