descr 412 Bytes
Newer Older
1 2 3 4 5 6 7 8
A support library for verified Coq parsers produced by Menhir

The Menhir parser generator, in --coq mode, can produce Coq parsers.
These parsers must be linked against this library, which provides
both an interpreter (which allows running the generated parser) and
a validator (which allows verifying, at parser construction time,
that the generated parser is correct and complete with respect to
the grammar).