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 1c7fd050f1..7724d7433c 100644 --- a/doc/sphinx/proofs/writing-proofs/index.rst +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -4,7 +4,7 @@ Basic proof writing =================== -|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 |