aboutsummaryrefslogtreecommitdiffhomepage
path: root/README.md
diff options
context:
space:
mode:
Diffstat (limited to 'README.md')
-rw-r--r--README.md3
1 files changed, 3 insertions, 0 deletions
diff --git a/README.md b/README.md
index 2329b536b..a41ee7cc0 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.