diff options
| author | notin | 2008-02-14 15:15:05 +0000 |
|---|---|---|
| committer | notin | 2008-02-14 15:15:05 +0000 |
| commit | 4a8cfa68ced0600d96766a90516411c9c8ea9166 (patch) | |
| tree | 432566210cc162d8d3fd1ff1a72b42ffc9d52b6e | |
| parent | 921f0ef22fcd79e69486e0aec75e57f68dce661e (diff) | |
Reconnaissance des tokens dans les notations (suite à la revision r10562)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10567 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tools/coqdoc/pretty.mll | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 1a2c5d866d..e0d2a3c99c 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -638,6 +638,9 @@ and notation_bol = parse and notation = parse | nl { line_break(); notation_bol lexbuf } | '"' { char '"'; false } + | token + { let s = lexeme lexbuf in + symbol s; notation lexbuf } | _ { let c = lexeme_char lexbuf 0 in char c; notation lexbuf } |