blob: 17db827e8f95d2c236ffbe9003bf0fa2630bc4d9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
(*i*)
open Names
open Entries
open Libnames
open Libobject
open Lib
(*i*)
(*s This modules provides official fucntions to declare modules and
module types *)
(*s Modules *)
val declare_module : identifier -> module_entry -> unit
val start_module :
identifier -> identifier list -> (mod_bound_id * module_type_entry) list
-> module_type_entry option -> unit
val end_module : identifier -> unit
(*s Module types *)
val declare_modtype : identifier -> module_type_entry -> unit
val start_modtype :
identifier -> identifier list -> (mod_bound_id * module_type_entry) list
-> unit
val end_modtype : identifier -> unit
(*s Objects of a module. They come in two lists: the substitutive ones
and the other *)
val module_objects : module_path -> library_segment
(*s Libraries i.e. modules on disk *)
type library_name = dir_path
type library_objects
val register_library :
library_name ->
Safe_typing.compiled_library -> library_objects -> Digest.t -> unit
val start_library : library_name -> unit
val export_library :
library_name -> Safe_typing.compiled_library * library_objects
(* [import_module mp] opens the module [mp] (in a Caml sense).
It modifies Nametab and performs the "open_object" function
for every object of the module. *)
val import_module : module_path -> unit
(*s [fold_all_segments] and [iter_all_segments] iterate over all
segments, the modules' segments first and then the current
segment. Modules are presented in an arbitrary order. The given
function is applied to all leaves (together with their section
path). The boolean indicates if we must enter closed sections. *)
val fold_all_segments : bool -> ('a -> object_name -> obj -> 'a) -> 'a -> 'a
val iter_all_segments : bool -> (object_name -> obj -> unit) -> unit
val debug_print_modtab : unit -> Pp.std_ppcmds
(*val debug_print_modtypetab : unit -> Pp.std_ppcmds*)
|
