diff options
author | 2016-10-08 22:51:09 +0200 | |
---|---|---|
committer | 2016-10-09 08:13:18 +0200 | |
commit | b8ae2de5be242bbd1e34ec974627c81f99b16d23 (patch) | |
tree | 6b6c2980e6aac60e53da6097dca7ae93db83d52e /tactics/hints.mli | |
parent | 8a8caba36ea6b0fd67e026ee3833d3b5b25af56d (diff) |
Moving Pp.comments to CLexer so that Pp is purer (no more side-effect
done by the Ppcmd_comment token) and so that lexing/parsing
side-effects are collected at the same place, i.e. in CLexer.
Diffstat (limited to 'tactics/hints.mli')
0 files changed, 0 insertions, 0 deletions