aboutsummaryrefslogtreecommitdiff
path: root/tools/coqdoc/index.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/index.mli')
-rw-r--r--tools/coqdoc/index.mli10
1 files changed, 5 insertions, 5 deletions
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 3649d6a4a2..517ec97a75 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -52,13 +52,9 @@ val init_coqlib_library : unit -> unit
val add_external_library : string -> coq_module -> unit
-(*s Scan identifiers introductions from a file *)
-
-val scan_file : 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 *)
@@ -69,6 +65,10 @@ type 'a index = {
val current_library : string ref
+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