aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaxime Dénès2018-01-25 13:43:14 +0100
committerMaxime Dénès2018-01-25 13:43:14 +0100
commit388b0adaa0fc3f52e80b562a0238dbc723b1b12f (patch)
tree29920eb3e7f731ae9a90124ee2660da2acc31958
parent05e0b45a254ab37e912e677d732aca20389263a8 (diff)
parent7ab89ea6d62f1a06c89b62cbd0688c159278047e (diff)
Merge PR #6626: [readme] Add DOI badge.
-rw-r--r--README.md1
1 files changed, 1 insertions, 0 deletions
diff --git a/README.md b/README.md
index fae83e02cf..883630acf1 100644
--- a/README.md
+++ b/README.md
@@ -4,6 +4,7 @@
[![Appveyor](https://ci.appveyor.com/api/projects/status/eln43k05pa2vm908/branch/master?svg=true)](https://ci.appveyor.com/project/coq/coq/branch/master)
[![Circle CI](https://circleci.com/gh/coq/coq/tree/master.svg?style=shield)](https://circleci.com/gh/coq/workflows/coq/tree/master)
[![Gitter](https://badges.gitter.im/coq/coq.svg)](https://gitter.im/coq/coq)
+[![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.1003420.svg)](https://doi.org/10.5281/zenodo.1003420)
Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an