diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-28 13:49:22 +0200 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-28 13:58:38 +0200 |
commit | ffeefb4b969aaa0b6728e701593b79250eac1c25 (patch) | |
tree | f6a8ccf3703921e8b2188a8a0a02c0ce47e6cbd5 /tools/coqdoc | |
parent | d065ea30843729c70e3b501a331d11499ad197e7 (diff) |
Recognize Parameters as a command in coqdoc. (Fix for bug #3279)
Diffstat (limited to 'tools/coqdoc')
-rw-r--r-- | tools/coqdoc/cpretty.mll | 2 |
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" |