get rid of gragrep, matitamake(Lib) and development windows,

[helm.git] / matita / matitac.ml

diff --git a/matita/matitac.ml b/matita/matitac.ml
index 868326a8dec808c68d1781bea0b3191d83f81d50..8f8a19b2da8c94e43082b54b6ec02497d1d76a4f 100644 (file)
--- a/matita/matitac.ml
+++ b/matita/matitac.ml
@@ -135,17 +135,7 @@ let main_compiler () =
         with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
       ;;
   
-      let build fname = 
-        let oldfname = 
-          Helm_registry.get_opt
-           Helm_registry.string "matita.filename"
-        in
-        let rc = MatitacLib.compile fname in
-        (match oldfname with
-        | Some n -> Helm_registry.set_string "matita.filename" n;
-        | _ -> Helm_registry.unset "matita.filename");
-        rc
-      ;;
+      let build = MatitacLib.compile;;
     end 
   in
   let module Make = Make.Make(F) in
@@ -155,12 +145,9 @@ let main_compiler () =
 let main () =
  Helm_registry.set_bool "matita.moo" true;
  match Filename.basename Sys.argv.(0) with
- |"gragrep"    |"gragrep.opt"    |"gragrep.opt.static"    ->Gragrep.main()
  |"matitadep"  |"matitadep.opt"  |"matitadep.opt.static"  ->Matitadep.main()
  |"matitaclean"|"matitaclean.opt"|"matitaclean.opt.static"->Matitaclean.main()
- |"matitamake" |"matitamake.opt" |"matitamake.opt.static" ->Matitamake.main()
- |"matitaprover"|"matitaprover.opt"
- |"matitaprover.opt.static" ->Matitaprover.main()
+ |"matitaprover"|"matitaprover.opt"|"matitaprover.opt.static"->Matitaprover.main()
  |"matitawiki"|"matitawiki.opt" ->MatitaWiki.main()
  | _ ->
     let dump_msg = "<filename> Dump with expanded macros to <filename>" in