From 979b9591ce5422cdf5ad76e4b6109b50cce4f1c7 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 27 Nov 2018 16:10:25 +0100
Subject: Move content of README-V1-V5 to Credits chapter.

---
 doc/sphinx/proof-engine/proof-handling.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 2300a317f1..27360f02d3 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -30,7 +30,7 @@ When a proof is completed, the message ``Proof completed`` is displayed.
 One can then register this proof as a defined constant in the
 environment. Because there exists a correspondence between proofs and
 terms of λ-calculus, known as the *Curry-Howard isomorphism*
-:cite:`How80,Bar81,Gir89,Hue88`, |Coq| stores proofs as terms of |Cic|. Those
+:cite:`How80,Bar81,Gir89,H89`, |Coq| stores proofs as terms of |Cic|. Those
 terms are called *proof terms*.
 
 
-- 
cgit v1.2.3