Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
768 B · 26 lines
at master
123456789101112131415161718192021222324252627(* The main file included in the OCaml toplevel. *)
#use "ml_toplevel/include_directories";;#use "ml_toplevel/include_printers";;#use "ml_toplevel/include_utilities";;
let go () = Flags.with_option Toploop.may_trace (fun () -> Coqloop.ml_toplevel_state := Some (Coqloop.loop ~state:(Option.get !Coqloop.ml_toplevel_state))) (); print_newline ()
let () = if not !Coqloop.ml_toplevel_include_ran then Toploop.add_directive "go" (Toploop.Directive_none go) Toploop.{section="Coq"; doc="Run Rocq toplevel loop"}
let _ = print_newline (); print_endline "OCaml toplevel with Rocq printers and utilities (to go back to Rocq, use `#quit;;`, or `#go;;` if `#trace` was used)"
let _ = Coqloop.ml_toplevel_include_ran := true