aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/github-check-prs.py
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-02-21 12:46:22 -0500
committerEmilio Jesus Gallego Arias2020-03-25 23:45:01 -0400
commitf374c2562b9522bd90330f6f17f0a7e41c723e8b (patch)
tree3ad126603fb6a7eccb1ec20b3dc3dd340cf22b90 /dev/tools/github-check-prs.py
parentaf7628468d638c77fb3f55a9eb315b687b76a21d (diff)
[parsing] Move `coq_parsable` custom logic to Grammar.
Latest refactorings allow us to make the signature Coq parser a standard `Grammar.S` one; the only bit needed is to provide the extra capabilities to the `Lexer` signature w.r.t. to comments state. The handling of Lexer state is still a bit ad-hoc, in particular it is global whereas it should be fully attached to the parsable. This may work ok in batch mode but the current behavior may be buggy in the interactive context. This PR doesn't solve that but it is a step towards a more functional solution.
Diffstat (limited to 'dev/tools/github-check-prs.py')
0 files changed, 0 insertions, 0 deletions