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 /tools/coqdoc/index.mli | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'tools/coqdoc/index.mli')
| -rw-r--r-- | tools/coqdoc/index.mli | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 56a3cd11..517ec97a 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) +(*i $Id$ i*) open Cdglobals type loc = int -type entry_type = +type entry_type = | Library | Module | Definition @@ -33,7 +33,7 @@ type entry_type = val type_name : entry_type -> string -type index_entry = +type index_entry = | Def of string * entry_type | Ref of coq_module * string * entry_type | Mod of coq_module * string @@ -44,28 +44,32 @@ val find_string : coq_module -> string -> index_entry val add_module : coq_module -> unit -type module_kind = Local | Coqlib | Unknown +type module_kind = Local | External of coq_module | Unknown val find_module : coq_module -> module_kind -(*s Scan identifiers introductions from a file *) +val init_coqlib_library : unit -> unit -val scan_file : string -> coq_module -> unit +val add_external_library : string -> coq_module -> unit (*s Read globalizations from a file (produced by coqc -dump-glob) *) -val read_glob : string -> coq_module +val read_glob : string -> unit (*s Indexes *) -type 'a index = { +type 'a index = { idx_name : string; idx_entries : (char * (string * 'a) list) list; idx_size : int } val current_library : string ref -val all_entries : unit -> +val display_letter : char -> string + +val prepare_entry : string -> entry_type -> string + +val all_entries : unit -> (coq_module * entry_type) index * (entry_type * coq_module index) list |