diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/changes.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/refman-preamble.rst | 4 |
3 files changed, 21 insertions, 17 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 0148925247..b6fcf9da22 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -198,21 +198,21 @@ Melquiond, Matthieu Sozeau, Enrico Tassi (who migrated it to opam 2) with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. -The 61 contributors to this version are David A. Dalrymple, Tanaka -Akira, Benjamin Barenblat, Yves Bertot, Frédéric Besson, Lasse -Blaauwbroek, Martin Bodin, Joachim Breitner, Tej Chajed, Frédéric -Chapoton, Arthur Charguéraud, Cyril Cohen, Lukasz Czajka, Christian -Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Gaëtan Gilbert, Matěj -Grabovský, Simon Gregersen, Jason Gross, Samuel Gruetter, Hugo Herbelin, -Jasper Hugunin, Mirai Ikebuchi, Emilio Jesus Gallego Arias, Chantal -Keller, Matej Košík, Vincent Laporte, Olivier Laurent, Larry Darryl Lee -Jr, Pierre Letouzey, Nick Lewycky, Yao Li, Yishuai Li, Xia Li-yao, Assia -Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez, Guillaume -Melquiond, Kayla Ngan, Sam Pablo Kuper, Karl Palmskog, Clément -Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, Kazuhiko Sakaguchi, Ryan -Scott, Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau, -Enrico Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo -Winterhalter, Beta Ziliani and Théo Zimmermann. +The 61 contributors to this version are Tanaka Akira, Benjamin +Barenblat, Yves Bertot, Frédéric Besson, Lasse Blaauwbroek, Martin +Bodin, Joachim Breitner, Tej Chajed, Frédéric Chapoton, Arthur +Charguéraud, Cyril Cohen, Lukasz Czajka, David A. Dalrymple, Christian +Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Emilio Jesus Gallego +Arias, Gaëtan Gilbert, Matěj Grabovský, Simon Gregersen, Jason Gross, +Samuel Gruetter, Hugo Herbelin, Jasper Hugunin, Mirai Ikebuchi, +Chantal Keller, Matej Košík, Sam Pablo Kuper, Vincent Laporte, Olivier +Laurent, Larry Darryl Lee Jr, Nick Lewycky, Yao Li, Yishuai Li, Assia +Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez, +Guillaume Melquiond, Kayla Ngan, Karl Palmskog, Pierre-Marie Pédrot, +Clément Pit-Claudel, Pierre Roux, Kazuhiko Sakaguchi, Ryan Scott, +Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau, Enrico +Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo Winterhalter, +Xia Li-yao, Beta Ziliani and Théo Zimmermann. Many power users helped to improve the design of the new features via the issue and pull request system, the |Coq| development mailing list, diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 47ecfb9db0..9e219bd503 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -62,7 +62,7 @@ A simple example of a ``_CoqProject`` file follows: theories/foo.v theories/bar.v -I src/ - src/baz.ml4 + src/baz.mlg src/bazaux.ml src/qux_plugin.mlpack @@ -111,7 +111,7 @@ decide how to build them. In particular: + |Coq| files must use the ``.v`` extension + |OCaml| files must use the ``.ml`` or ``.mli`` extension + |OCaml| files that require pre processing for syntax - extensions (like ``VERNAC EXTEND``) must use the ``.ml4`` extension + extensions (like ``VERNAC EXTEND``) must use the ``.mlg`` extension + In order to generate a plugin one has to list all |OCaml| modules (i.e. ``Baz`` for ``baz.ml``) in a ``.mlpack`` file (or ``.mllib`` file). diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst index c662028773..de95eda989 100644 --- a/doc/sphinx/refman-preamble.rst +++ b/doc/sphinx/refman-preamble.rst @@ -70,7 +70,11 @@ .. |p_i| replace:: `p`\ :math:`_{i}` .. |p_n| replace:: `p`\ :math:`_{n}` .. |Program| replace:: :strong:`Program` +.. |Prop| replace:: :math:`\Prop` +.. |SProp| replace:: :math:`\SProp` +.. |Set| replace:: :math:`\Set` .. |SSR| replace:: :smallcaps:`SSReflect` +.. |Type| replace:: :math:`\Type` .. |t_1| replace:: `t`\ :math:`_{1}` .. |t_i| replace:: `t`\ :math:`_{i}` .. |t_m| replace:: `t`\ :math:`_{m}` |