From 62ca663881ac7f731e2cf8a574c2e615f8d4a900 Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Wed, 5 Aug 2015 16:16:13 +0200 Subject: README in MarkDown --- README | 66 --------------------------------------------------------------- README.md | 41 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 41 insertions(+), 66 deletions(-) delete mode 100644 README create mode 100644 README.md diff --git a/README b/README deleted file mode 100644 index 293ee4c8f2..0000000000 --- a/README +++ /dev/null @@ -1,66 +0,0 @@ - - THE COQ V8 SYSTEM - ================= - -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 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 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 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 - - http://coq.inria.fr/bugs - - To be effective, bug reports should mention the Caml 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. diff --git a/README.md b/README.md new file mode 100644 index 0000000000..3c9ebcb3f0 --- /dev/null +++ b/README.md @@ -0,0 +1,41 @@ +# THE COQ V8 SYSTEM + +## 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 From c3d1ca3e0957d6380143bdce29bfccbe1b05f537 Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Wed, 5 Aug 2015 16:19:07 +0200 Subject: Simpler titles --- README.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 3c9ebcb3f0..2329b536bf 100644 --- a/README.md +++ b/README.md @@ -1,22 +1,22 @@ -# THE COQ V8 SYSTEM +# Coq -## INSTALLATION +## Installation See the file `INSTALL` for installation procedure. -## DOCUMENTATION +## 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 +## 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 +## Availability Coq is available from [coq.inria.fr](http://coq.inria.fr). -## THE COQ CLUB +## 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). @@ -33,7 +33,7 @@ The topics to be discussed in the club should include: For any questions/suggestions about the Coq Club, please write to `coq-club-request@inria.fr`. -## BUGS REPORT +## 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 -- cgit v1.2.3 From 0446b632883e7baa6979bd0251258ea3769c337b Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Wed, 5 Aug 2015 16:20:41 +0200 Subject: Description added --- README.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/README.md b/README.md index 2329b536bf..a41ee7cc07 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,7 @@ # 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. -- cgit v1.2.3