diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /toplevel/mltop.mli | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'toplevel/mltop.mli')
-rw-r--r-- | toplevel/mltop.mli | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 875fb423..4230f0ee 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mltop.mli 11528 2008-10-31 08:40:42Z glondu $ i*) +(*i $Id$ i*) -(* If there is a toplevel under Coq, it is described by the following +(* If there is a toplevel under Coq, it is described by the following record. *) -type toplevel = { +type toplevel = { load_obj : string -> unit; use_file : string -> unit; add_dir : string -> unit; @@ -48,9 +48,6 @@ val add_rec_ml_dir : string -> unit val add_path : unix_path:string -> coq_root:Names.dir_path -> unit val add_rec_path : unix_path:string -> coq_root:Names.dir_path -> unit -val add_init_with_state : (unit -> unit) -> unit -val init_with_state : unit -> unit - (* List of modules linked to the toplevel *) val add_known_module : string -> unit val module_is_known : string -> bool @@ -62,11 +59,15 @@ val add_loaded_module : string -> unit val init_ml_modules : unit -> unit val unfreeze_ml_modules : string list -> unit -type ml_module_object = { mnames: string list } +type ml_module_object = { + mlocal: Vernacexpr.locality_flag; + mnames: string list; +} val inMLModule : ml_module_object -> Libobject.obj val outMLModule : Libobject.obj -> ml_module_object -val declare_ml_modules : string list -> unit +val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit + val print_ml_path : unit -> unit val print_ml_modules : unit -> unit |