This repository contains an AST and pretty-printer for Coq. The code in this repository has originally been developed as part of the hs-to-coq compiler but has been extracted for use in the free-compiler

1. Directory Structure
2. Getting Started
3. Get Involved
4. License

This repository is structured as follows.

• ./src/lib contains the source code of the library. All modules start with the prefix Language.Coq.

  • The AST is located in Language.Coq.Gallina.
  • The pretty-printer can be found in Language.Coq.Pretty.

• tool contains Bash scripts that are used during development and for testing.

The library is written in Haskell and uses Cabal to manage the dependencies. The library has been tested with the following versions of the GHC and Cabal.

• GHC, version 8.6.5
• Cabal, version 3.4.0.0

The language-coq package is not yet on Hackage. In order to use this package in your own project, include the following stanza in your cabal.project file.

source-repository-package
  type: git
  location: git://github.com/FreeProving/language-coq.git
  tag: v0.4.0.0

Feature requests, enhancement proposals, bug reports, pull requests and all other contributions are welcome!
Have a look at our contributing guidelines for more information on how to contribute.

The language-coq library is licensed under the MIT License.
See the LICENSE file for details.