From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 10 Nov 2004 12:02:21 +0000 (+0000)
Subject: parse Baseuri command
X-Git-Tag: v_0_6_4_1~3
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc399fb172ecd3b598844a99eefb817ee0675e3d;hp=17f92a5a11a70bd4eb0ae3f5108160792167e7bb;p=helm.git

parse Baseuri command
---

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)
     ]