diff options
Diffstat (limited to 'doc/sphinx/proofs')
| -rw-r--r-- | doc/sphinx/proofs/creating-tactics/index.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/index.rst | 2 |
2 files changed, 6 insertions, 6 deletions
diff --git a/doc/sphinx/proofs/creating-tactics/index.rst b/doc/sphinx/proofs/creating-tactics/index.rst index 1af1b0b726..f1d4fa789d 100644 --- a/doc/sphinx/proofs/creating-tactics/index.rst +++ b/doc/sphinx/proofs/creating-tactics/index.rst @@ -18,13 +18,13 @@ new tactics: - `Mtac2 <https://github.com/Mtac2/Mtac2>`_ is an external plugin which provides another typed tactic language. While Ltac2 belongs - to the ML language family, Mtac2 reuses the language of Coq itself - as the language to build Coq tactics. + to the ML language family, Mtac2 reuses the language of |Coq| itself + as the language to build |Coq| tactics. - The most traditional way of building new complex tactics is to write - a Coq plugin in OCaml. Beware that this also requires much more - effort and commitment. A tutorial for writing Coq plugins is - available in the Coq repository in `doc/plugin_tutorial + a |Coq| plugin in |OCaml|. Beware that this also requires much more + effort and commitment. A tutorial for writing |Coq| plugins is + available in the |Coq| repository in `doc/plugin_tutorial <https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_. .. toctree:: 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 |