Parser Validator

A standalone version of the parser validator library in CompCert, as used by Coq code generated by Menhir.

Requirements

First run ./configure in the root directory, and then run make.

Name		Name	Last commit message	Last commit date
Latest commit History 2 Commits
Alphabet.v		Alphabet.v
Automaton.v		Automaton.v
Grammar.v		Grammar.v
Interpreter.v		Interpreter.v
Interpreter_complete.v		Interpreter_complete.v
Interpreter_correct.v		Interpreter_correct.v
Interpreter_safe.v		Interpreter_safe.v
Main.v		Main.v
Makefile		Makefile
README.md		README.md
Tuples.v		Tuples.v
Validator_complete.v		Validator_complete.v
Validator_safe.v		Validator_safe.v
configure		configure
coqproject.sh		coqproject.sh