diff options
| author | Théo Zimmermann | 2020-11-09 18:39:49 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-09 18:39:49 +0100 |
| commit | a3869e5371c89629ddfd8ccdd1bdc0de12efe806 (patch) | |
| tree | d2791aae79a76984f76989bd560989dd0faff8a2 /doc/sphinx/proofs/creating-tactics | |
| parent | 87523f151484dcc4eff4f04535b9356036b51a3d (diff) | |
[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.
The smallcaps rendering was inexistent in the PDF version and did not
look good in the HTML version.
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 f1d4fa789d..1af1b0b726 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:: |