diff options
| author | Jason Gross | 2019-10-14 12:47:57 -0400 |
|---|---|---|
| committer | Jason Gross | 2019-10-14 12:47:57 -0400 |
| commit | 911accd83d0161d1587652af9ec5365943023c98 (patch) | |
| tree | 3f5c043454728a250bdfef98eea788f7e615dc18 /doc | |
| parent | 2169cf83775a57f48fe1b55796b5bc026a11aea6 (diff) | |
| parent | 3e0bf68bdc1ac6bde7bd04236657fb4d554817ad (diff) | |
Merge PR #10883: Doc update with mlg extension - fix #10855
Reviewed-by: JasonGross
Reviewed-by: gares
Ack-by: ppedrot
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). |