diff options
| author | Théo Zimmermann | 2020-10-19 16:06:30 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-10-20 11:07:52 +0200 |
| commit | 3230c568eb0bc719feca642a1537555e262478eb (patch) | |
| tree | 8d88af13db13ccf36fbe32826e711415c671e93a /doc/sphinx/proofs/creating-tactics | |
| parent | 7b07bc9aac0f7f990b8b12e7120d7a4e0bcd4fee (diff) | |
Add some missing smallcaps.
Diffstat (limited to 'doc/sphinx/proofs/creating-tactics')
| -rw-r--r-- | doc/sphinx/proofs/creating-tactics/index.rst | 10 |
1 files changed, 5 insertions, 5 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:: |