X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=9eb1dbf69c608c9ba231d4e46f45f3ae78fb1f18;hb=81b43e348e0c3e61114900d1e1df058ecc68cd90;hp=8ab94d979b05e67a3e4aeef96067ef9c81db6b44;hpb=4db221ee87ba30f63db0ea32c98858041e8e6213;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 8ab94d979..9eb1dbf69 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -60,14 +60,6 @@ let first_line s =
     String.sub s 0 nl_pos
   with Not_found -> s
 
-  (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
-let goal_ast n =
-  let module A = GrafiteAst in
-  let loc = HExtlib.dummy_floc in
-  A.Executable (loc, A.Tactical (loc,
-    A.Tactic (loc, A.Goal (loc, n)),
-    Some (A.Dot loc)))
-
 type guistuff = {
   mathviewer:MatitaTypes.mathViewer;
   urichooser: UriManager.uri list -> UriManager.uri list;
@@ -255,10 +247,9 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
       | [uri] -> 
           let suri = UriManager.string_of_uri uri in
           let ast loc =
-            TA.Executable (loc, (TA.Tactical (loc,
-              TA.Tactic (loc,
-                TA.Apply (loc, CicNotationPt.Uri (suri, None))),
-                Some (TA.Dot loc)))) in
+            TA.Executable (loc, (TA.Tactic (loc,
+             Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))),
+             TA.Dot loc))) in
           let text =
            comment parsed_text ^ "\n" ^
             pp_eager_statement_ast (ast HExtlib.dummy_floc) in