parse Baseuri command

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 53559bcd298e8cb80a7be1fc7a9cd62d5381fafc..775f13f7d7e0f8803baa7f1a58f9408fd17cc8fa 100644 (file)
--- 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)
     ]