aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/index.mli
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-09-25 20:49:48 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-09-25 20:49:48 +0000
commit60f775dc72df750a6197389fbd0a468636a66f56 (patch)
tree43d6e506702437abd58479e4c8553158075afb5f /tools/coqdoc/index.mli
parente3535ade2bd4c7b75ec093e9e0f124f84c506b8f (diff)
Improvements in coqdoc:
- Better handling of spaces by actually ignoring what's inside proof scripts in light/gallina mode (detection of [Proof with] vs [Proof.] vs [Proof t.] and [Qed]/[Save]/...). - Provide fancy replacements for forall,/\,... etc in HTML in case the utf8 option is on. - Use typesetting information in HTML output and customize the CSS accordingly. The default color scheme follows closely the one set by Conor for Epigram; of course one can change it. - A try at interpolating identifiers in comments if they are defined in the same module, with a corresponding flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11421 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/index.mli')
-rw-r--r--tools/coqdoc/index.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 9831ca3cb..bfb57dad2 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -40,6 +40,8 @@ type index_entry =
val find : coq_module -> loc -> index_entry
+val find_string : coq_module -> string -> index_entry
+
val add_module : coq_module -> unit
type module_kind = Local | Coqlib | Unknown