matitaMisc.ml

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index e3dec088b4034ab8331e578814873c567dbe527f..f8a9c9bb132a3b23c0596d4b1778a701f06836d0 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -171,7 +171,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
         | `NO -> raise exc
         | `CANCEL -> do_nothing ())
       in
-      let handle_withoud_devel filename =
+      let handle_without_devel filename =
         let title = "Unable to include " ^ what in
         let message = 
          what ^ " is <b>not</b> handled by a development.\n" ^
@@ -189,11 +189,11 @@ let eval_with_engine guistuff status user_goal parsed_text st =
         | `CANCEL -> do_nothing())
       in
       match guistuff.filenamedata with
-      | None,None -> handle_withoud_devel None
+      | None,None -> handle_without_devel None
       | None,Some d -> handle_with_devel d
       | Some f,_ ->
           match MatitamakeLib.development_for_dir (Filename.dirname f) with
-          | None -> handle_withoud_devel (Some f)
+          | None -> handle_without_devel (Some f)
           | Some d -> handle_with_devel d
 ;;