diff options
Diffstat (limited to 'doc/sphinx/proofs/writing-proofs/index.rst')
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/index.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst index a279a5957f..3f5526dba8 100644 --- a/doc/sphinx/proofs/writing-proofs/index.rst +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -4,7 +4,7 @@ Writing proofs ============== -Coq is an interactive theorem prover, or proof assistant, which means +|Coq| is an interactive theorem prover, or proof assistant, which means that proofs can be constructed interactively through a dialog between the user and the assistant. The building blocks for this dialog are tactics which the user will use to represent steps in the proof of a |