package coq

  1. Overview
  2. Docs
package coq
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
type add_ml =
  1. | AddNoML
  2. | AddTopML
  3. | AddRecML
type vo_path_spec = {
  1. unix_path : string;
  2. coq_path : Names.DirPath.t;
  3. implicit : bool;
  4. has_ml : add_ml;
}
type coq_path_spec =
  1. | VoPath of vo_path_spec
  2. | MlPath of string
type coq_path = {
  1. path_spec : coq_path_spec;
  2. recursive : bool;
}
val add_coq_path : coq_path -> unit
val add_known_module : string -> unit
val module_is_known : string -> bool
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.t
val print_ml_modules : unit -> Pp.t
val print_gc : unit -> Pp.t