aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/index.mli
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-06 22:39:43 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-06 22:39:43 +0000
commita1fe45ddbd37d3c447a23cde0ee21f105ef42ac0 (patch)
tree648a977d3137ffa9c7cc97e8503c0a5d8620dbfa /tools/coqdoc/index.mli
parent0cdfa2fb137989f75cdebfa3a64726bc0d56a8af (diff)
Enhancements to coqdoc, better globalization of sections and modules.
Minor fix in Morphisms which prevented working with higher-order morphisms and PER relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11065 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/index.mli')
-rw-r--r--tools/coqdoc/index.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index ec04017c4..9831ca3cb 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -29,6 +29,7 @@ type entry_type =
| TacticDefinition
| Abbreviation
| Notation
+ | Section
val type_name : entry_type -> string