← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to toplevel/mltop.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
toplevel/mltop.mli
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: mltop.mli 11528 2008-10-31 08:40:42Z glondu $ i*)
 
10
 
 
11
(* If there is a toplevel under Coq, it is described by the following 
 
12
   record. *)
 
13
type toplevel = { 
 
14
  load_obj : string -> unit;
 
15
  use_file : string -> unit;
 
16
  add_dir  : string -> unit;
 
17
  ml_loop  : unit -> unit }
 
18
 
 
19
(* Sets and initializes a toplevel (if any) *)
 
20
val set_top : toplevel -> unit
 
21
 
 
22
(* Are we in a native version of Coq? *)
 
23
val is_native : bool
 
24
 
 
25
(* Removes the toplevel (if any) *)
 
26
val remove : unit -> unit
 
27
 
 
28
(* Tests if an Ocaml toplevel runs under Coq *)
 
29
val is_ocaml_top : unit -> bool
 
30
 
 
31
(* Tests if we can load ML files *)
 
32
val has_dynlink : bool
 
33
 
 
34
(* Starts the Ocaml toplevel loop *)
 
35
val ocaml_toploop : unit -> unit
 
36
 
 
37
(* Dynamic loading of .cmo *)
 
38
val dir_ml_load : string -> unit
 
39
 
 
40
(* Dynamic interpretation of .ml *)
 
41
val dir_ml_use : string -> unit
 
42
 
 
43
(* Adds a path to the ML paths *)
 
44
val add_ml_dir : string -> unit
 
45
val add_rec_ml_dir : string -> unit
 
46
 
 
47
(* Adds a path to the Coq and ML paths *)
 
48
val add_path : unix_path:string -> coq_root:Names.dir_path -> unit
 
49
val add_rec_path : unix_path:string -> coq_root:Names.dir_path -> unit
 
50
 
 
51
val add_init_with_state : (unit -> unit) -> unit
 
52
val init_with_state : unit -> unit
 
53
 
 
54
(* List of modules linked to the toplevel *)
 
55
val add_known_module : string -> unit
 
56
val module_is_known : string -> bool
 
57
val load_object : string -> string -> unit
 
58
 
 
59
(* Summary of Declared ML Modules *)
 
60
val get_loaded_modules : unit -> string list
 
61
val add_loaded_module : string -> unit
 
62
val init_ml_modules : unit -> unit
 
63
val unfreeze_ml_modules : string list -> unit
 
64
 
 
65
type ml_module_object = { mnames: string list }
 
66
val inMLModule : ml_module_object -> Libobject.obj
 
67
val outMLModule : Libobject.obj -> ml_module_object
 
68
 
 
69
val declare_ml_modules : string list -> unit
 
70
val print_ml_path : unit -> unit
 
71
 
 
72
val print_ml_modules : unit -> unit