diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /toplevel/mltop.mli | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'toplevel/mltop.mli')
-rw-r--r-- | toplevel/mltop.mli | 88 |
1 files changed, 0 insertions, 88 deletions
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli deleted file mode 100644 index 6633cb93..00000000 --- a/toplevel/mltop.mli +++ /dev/null @@ -1,88 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** {5 Toplevel management} *) - -(** If there is a toplevel under Coq, it is described by the following - record. *) -type toplevel = { - load_obj : string -> unit; - use_file : string -> unit; - add_dir : string -> unit; - ml_loop : unit -> unit } - -(** Sets and initializes a toplevel (if any) *) -val set_top : toplevel -> unit - -(** Are we in a native version of Coq? *) -val is_native : bool - -(** Removes the toplevel (if any) *) -val remove : unit -> unit - -(** Tests if an Ocaml toplevel runs under Coq *) -val is_ocaml_top : unit -> bool - -(** Starts the Ocaml toplevel loop *) -val ocaml_toploop : unit -> unit - -(** {5 ML Dynlink} *) - -(** Tests if we can load ML files *) -val has_dynlink : bool - -(** Dynamic loading of .cmo *) -val dir_ml_load : string -> unit - -(** Dynamic interpretation of .ml *) -val dir_ml_use : string -> unit - -(** Adds a path to the ML paths *) -val add_ml_dir : string -> unit -val add_rec_ml_dir : string -> unit - -type add_ml = AddNoML | AddTopML | AddRecML - -(** Adds a path to the Coq and ML paths *) -val add_rec_path : add_ml -> unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit - -(** List of modules linked to the toplevel *) -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 - -(** {5 Initialization functions} *) - -(** Declare a plugin and its initialization function. - A plugin is just an ML module with an initialization function. - Adding a known plugin implies adding it as a known ML module. - The initialization function is granted to be called after Coq is fully - bootstrapped, even if the plugin is statically linked with the toplevel *) -val add_known_plugin : (unit -> unit) -> string -> unit - -(** Calls all initialization functions in a non-specified order *) -val init_known_plugins : unit -> unit - -(** Register a callback that will be called when the module is declared with - the Declare ML Module command. This is useful to define Coq objects at that - time only. Several functions can be defined for one module; they will be - called in the order of declaration, and after the ML module has been - properly initialized. *) -val declare_cache_obj : (unit -> unit) -> string -> unit - -(** {5 Declaring modules} *) - -val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit - -(** {5 Utilities} *) - -val print_ml_path : unit -> Pp.std_ppcmds -val print_ml_modules : unit -> Pp.std_ppcmds -val print_gc : unit -> Pp.std_ppcmds |