diff options
| author | Clément Pit-Claudel | 2019-03-07 09:28:30 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-03-07 09:28:30 -0500 |
| commit | 29b85080afef1c83ee772de3e69c487627ae6ce5 (patch) | |
| tree | 1a9517a8c885a81587eae6eb9acbfaba417e0089 /doc/sphinx/proof-engine | |
| parent | c9fd99644e223ada3aad53915f1cd0d2598882b3 (diff) | |
| parent | 52b29f236ee2535257df1439740e5c86ed17e69d (diff) | |
Merge PR #9133: Move README-V1-V5 to credits chapter
Reviewed-by: cpitclaudel
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 2 |
1 files changed, 1 insertions, 1 deletions
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*. |