aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-04-28 13:49:22 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-04-28 13:58:38 +0200
commitffeefb4b969aaa0b6728e701593b79250eac1c25 (patch)
treef6a8ccf3703921e8b2188a8a0a02c0ce47e6cbd5 /tools/coqdoc
parentd065ea30843729c70e3b501a331d11499ad197e7 (diff)
Recognize Parameters as a command in coqdoc. (Fix for bug #3279)
Diffstat (limited to 'tools/coqdoc')
-rw-r--r--tools/coqdoc/cpretty.mll2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index b4328d700..73c313252 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -325,7 +325,7 @@ let def_token =
let decl_token =
"Hypothesis"
| "Hypotheses"
- | "Parameter"
+ | "Parameter" 's'?
| "Axiom" 's'?
| "Conjecture"