diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-02-11 08:23:26 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-02-11 08:23:26 +0100 |
| commit | 3761b6b17d43470902a221b4df77e5ca13c8021f (patch) | |
| tree | b0c1cc136937500e32289e412548b6e89bc0f284 /tools | |
| parent | 69ae6e7d1c591b173cb64578b194529411b90cea (diff) | |
Make coqdoc -l properly handle Local before Ltac. (Fix for bug #3307)
Diffstat (limited to 'tools')
| -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 edf7ee8e3..20dd69f82 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -405,7 +405,7 @@ let set_kw = let gallina_kw_to_hide = "Implicit" space+ "Arguments" - | "Ltac" + | ("Local" space+)? "Ltac" | "Require" | "Import" | "Export" |