Skip to content
Fetching contributors…
Cannot retrieve contributors at this time
57 lines (43 sloc) 1.86 KB
(* File to include to install the pretty-printers in the ocaml toplevel *)
(* Typical usage :
$ coqtop.byte # or even better : rlwrap coqtop.byte
Coq < Drop.
# #use "include";;
Alternatively, you can avoid typing #use "include" after each Drop
by adding the following lines in your $HOME/.ocamlinit :
if Filename.basename Sys.argv.(0) = "coqtop.byte"
then ignore (Toploop.use_silently Format.std_formatter "include")
*)
(* For OCaml 3.10.x:
clflags.cmi (a ocaml compilation by-product) must be in the library path.
On Debian, install ocaml-compiler-libs, and uncomment the following:
#directory "+compiler-libs/utils";;
Clflags.recursive_types := true;;
*)
#cd ".";;
#use "base_include";;
#install_printer (* pp_stdcmds *) pppp;;
#install_printer (* pattern *) pppattern;;
#install_printer (* glob_constr *) ppglob_constr;;
#install_printer (* constr *) ppconstr;;
#install_printer (* constr_substituted *) ppsconstr;;
#install_printer (* universe *) ppuni;;
#install_printer (* universes *) ppuniverses;;
#install_printer (* type_judgement *) pptype;;
#install_printer (* judgement *) ppj;;
#install_printer (* hint_db *) print_hint_db;;
(*#install_printer (* hints_path *) pphintspath;;*)
#install_printer (* goal *) ppgoal;;
(*#install_printer (* sigma goal *) ppsigmagoal;;*)
(*#install_printer (* proof *) pproof;;*)
#install_printer (* Goal.goal *) ppgoalgoal;;
#install_printer (* metaset.t *) ppmetas;;
#install_printer (* evar_map *) ppevm;;
#install_printer (* ExistentialSet.t *) ppexistentialset;;
#install_printer (* clenv *) ppclenv;;
#install_printer (* env *) ppenv;;
#install_printer (* tactic *) pptac;;
#install_printer (* object *) ppobj;;
#install_printer (* global_reference *) ppglobal;;
#install_printer (* generic_argument *) pp_generic_argument;;
#install_printer (* fconstr *) ppfconstr;;
Something went wrong with that request. Please try again.