matitac now compiles like make (recorsively) if needed.

[helm.git] / matita / matitac.ml

diff --git a/matita/matitac.ml b/matita/matitac.ml
index 179a0ba8e8e508e413f22958cef5c20cc1039fbc..d603d1b85d9909381f003d5aa8e6e5e7d6458396 100644 (file)
--- a/matita/matitac.ml
+++ b/matita/matitac.ml
@@ -98,13 +98,9 @@ let main () =
  |"matitaprover.opt.static" ->Matitaprover.main()
  |"matitawiki"|"matitawiki.opt" ->MatitaWiki.main()
  | _ ->
-(*
-      let _ = Paramodulation.Saturation.init () in  *)
-(* ALB to link paramodulation *)
       let dump_msg = "<filename> Dump source with expanded macros to <filename>" in
       MatitaInit.add_cmdline_spec ["-dump", Arg.String dump, dump_msg];
-      let _ = MatitacLib.main `COMPILER in
-      ()
+      MatitacLib.main ()
 
 let _ = main ()