X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=48cc9111bdad5c9c8511ef8f36d35ef1ee3a4145;hb=8ab7608b1f6e6c4babea0f9d0a771e350d481229;hp=811b1a858a4b98f873445d76ee4d247d08f8f834;hpb=db88f09dfd6da59000c93e2ea1ea8565ec8e101d;p=helm.git

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 811b1a858..48cc9111b 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -108,7 +108,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
       | TA.Command (_, TA.Include _) -> DisambiguateTypes.Environment.empty
       | _ -> MatitaSync.alias_diff ~from:status new_status
   in
-  (* we remove the defined object since we consider them "automathic aliases" *)
+  (* we remove the defined object since we consider them "automatic aliases" *)
   let new_aliases = 
     let module DTE = DisambiguateTypes.Environment in
     let module UM = UriManager in
@@ -467,6 +467,7 @@ object (self)
   val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"]
 
   method locked_mark = locked_mark
+  method locked_tag = locked_tag
 
     (* history can't be empty, the invariant above grant that it contains at
      * least the init status *)