aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-03-06 00:35:26 +0000
committerGravatar thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-03-06 00:35:26 +0000
commitd1a73c9a47d554c3cf687f2ed10ace5671d1e6c1 (patch)
treec87afe46039ec4ab55d487754738cca90c53694f /tools
parent6b010da9faf1c4d1b214505daf8ecf9ea6afbd33 (diff)
Adding Function as keyword for coqdoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12847 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/cpretty.mll1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 64cd5ff55..071b3d555 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -329,6 +329,7 @@ let def_token =
| "Example"
| "Local"
| "Fixpoint"
+ | "Function"
| "Boxed"
| "CoFixpoint"
| "Record"