]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/.ocamlinit
bugfix: "LPAREN" vs LPAREN
[helm.git] / 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 ;;