Big changes:

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 86775f2923dcb041b606c8d30a303d912c7115f0..f339ebb40f3547756b9349666d1637408b98371d 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -149,8 +149,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
   with
     MatitaEngine.UnableToInclude what as exc ->
       let compile_needed_and_go_on d =
-        let root = MatitamakeLib.root_for_development d in
-        let target = root ^ "/" ^ what in
+        let target = what in
         let refresh_cb () = 
           while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
         in
@@ -334,10 +333,10 @@ let eval_executable guistuff status user_goal parsed_text script ex =
   match ex with
   | TA.Command (loc, _) | TA.Tactical (loc, _) ->
       (try 
-        (match ML.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
+        (match MatitaMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
         | None -> ()
         | Some u -> 
-            if not (ML.is_empty u) then
+            if not (MatitaMisc.is_empty u) then
               match 
                 guistuff.ask_confirmation 
                   ~title:"Baseuri redefinition"