From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- README.md | 44 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 README.md (limited to 'README.md') diff --git a/README.md b/README.md new file mode 100644 index 00000000..a41ee7cc --- /dev/null +++ b/README.md @@ -0,0 +1,44 @@ +# Coq +Coq is a formal proof management system. It provides a formal language to write +mathematical definitions, executable algorithms and theorems together with an +environment for semi-interactive development of machine-checked proofs. + +## Installation +See the file `INSTALL` for installation procedure. + +## Documentation +The documentation is part of the archive in directory doc. The +documentation of the last released version is available on the Coq +web site at [coq.inria.fr/doc](http://coq.inria.fr/doc). + +## Changes +There is a file named `CHANGES` that explains the differences and the +incompatibilities since last versions. If you upgrade Coq, please read +it carefully. + +## Availability +Coq is available from [coq.inria.fr](http://coq.inria.fr). + +## The Coq Club +The Coq Club moderated mailing list is meant to be a standard way +to discuss questions about the Coq system and related topics. The +subscription link can be found at [coq.inria.fr/community](http://coq.inria.fr/community). + +The topics to be discussed in the club should include: + +* technical problems; +* questions about proof developments; +* suggestions and questions about the implementation; +* announcements of proofs; +* theoretical questions about typed lambda-calculi which are + closely related to Coq. + +For any questions/suggestions about the Coq Club, please write to +`coq-club-request@inria.fr`. + +## Bugs report +Send your bug reports by filling a form at [coq.inria.fr/bugs](http://coq.inria.fr/bugs). + +To be effective, bug reports should mention the OCaml version used +to compile and run Coq, the Coq version (`coqtop -v`), the configuration +used, and include a complete source example leading to the bug. -- cgit v1.2.3