helm/matita/.ocamlinit

   1 (* directories *)
   2 #directory "../ocaml/cic"
   3 #directory "../ocaml/cic_notation"
   4 #directory "../ocaml/cic_omdoc"
   5 #directory "../ocaml/cic_proof_checking"
   6 #directory "../ocaml/cic_textual_parser2"
   7 #directory "../ocaml/cic_transformations"
   8 #directory "../ocaml/cic_unification"
   9 #directory "../ocaml/getter"
  10 #directory "../ocaml/hbugs"
  11 #directory "../ocaml/mathql"
  12 #directory "../ocaml/mathql_generator"
  13 #directory "../ocaml/mathql_interpreter"
  14 #directory "../ocaml/metadata"
  15 #directory "../ocaml/paramodulation"
  16 #directory "../ocaml/registry"
  17 #directory "../ocaml/tactics"
  18 #directory "../ocaml/thread"
  19 #directory "../ocaml/urimanager"
  20 #directory "../ocaml/xml"
  21 #directory "../ocaml/xmldiff"
  22
  23 (* custom printers *)
  24 let fppuri ppf uri =
  25  let s = UriManager.string_of_uri uri in
  26   Format.pp_print_string ppf s
  27 ;;
  28
  29 #install_printer CicMetaSubst.fppsubst;;
  30 #install_printer CicMetaSubst.fppterm;;
  31 #install_printer CicMetaSubst.fppmetasenv;;
  32 #install_printer fppuri;;
  33
  34 (* utility functions *)
  35 let go = MatitacLib.interactive_loop;;
  36
  37 (* let's go! *)
  38 let _ =
  39  at_exit (fun () -> MatitacLib.clean_exit None);
  40  if Array.length Sys.argv > 1 then
  41    MatitacLib.main `TOPLEVEL
  42  else
  43    MatitacLib.go ()
  44 ;;