Module Coq

module Grammar : sig ... end

This module provides functionality onijn's "compiler". We need to generate string constructs that can be parsed by Coq in order to generate a proof-script that can be checked. The functions in this module produce strings that satisfy the requirements in https://coq.inria.fr/distrib/current/refman/language/core/definitions.html.

module Proof_script : sig ... end

This module provide specialized functionality for the generation of Coq proof scripts.