diff options
| author | mcaci | 2019-10-12 14:24:18 +0200 |
|---|---|---|
| committer | mcaci | 2019-10-13 22:02:02 +0200 |
| commit | 3e0bf68bdc1ac6bde7bd04236657fb4d554817ad (patch) | |
| tree | ddf580dcee22c42fcb0a10c3b7ef279f2b0f211d /doc | |
| parent | e8d0b5a8856a695dc3f6a28e2d305c095ef50c19 (diff) | |
Doc update with mlg extension - fix #10855
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 4 |
1 files changed, 2 insertions, 2 deletions
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). |