summaryrefslogtreecommitdiff
path: root/tools/coqdoc/index.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/index.mli')
-rw-r--r--tools/coqdoc/index.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 8c658a90..0f62a086 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -34,10 +34,11 @@ val type_name : entry_type -> string
type index_entry =
| Def of string * entry_type
| Ref of coq_module * string * entry_type
- | Mod of coq_module * string
+(* Find what symbol coqtop said is located at loc in the source file *)
val find : coq_module -> loc -> index_entry
+(* Find what data is referred to by some string in some coq module *)
val find_string : coq_module -> string -> index_entry
val add_module : coq_module -> unit