package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type toplevel = {
  1. load_obj : string -> unit;
  2. use_file : string -> unit;
  3. add_dir : string -> unit;
  4. ml_loop : unit -> unit;
}
val set_top : toplevel -> unit
val is_native : bool
val remove : unit -> unit
val is_ocaml_top : unit -> bool
val ocaml_toploop : unit -> unit
val dir_ml_load : string -> unit
val dir_ml_use : string -> unit
val add_ml_dir : string -> unit
val add_rec_ml_dir : string -> unit
type add_ml =
  1. | AddNoML
  2. | AddTopML
  3. | AddRecML
val add_rec_path : add_ml -> unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
val add_known_module : string -> unit
val module_is_known : string -> bool
val load_ml_object : string -> string -> unit
val load_ml_object_raw : string -> unit
val load_ml_objects_raw_rex : Str.regexp -> unit
val add_known_plugin : (unit -> unit) -> string -> unit
val init_known_plugins : unit -> unit
val declare_cache_obj : (unit -> unit) -> string -> unit
val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit
val print_ml_path : unit -> Pp.std_ppcmds
val print_ml_modules : unit -> Pp.std_ppcmds
val print_gc : unit -> Pp.std_ppcmds
OCaml

Innovation. Community. Security.