diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-26 11:33:14 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-26 11:33:14 +0200 |
| commit | 5aa07e9eb97f6233f47aa8a79fb0890fca14f427 (patch) | |
| tree | 7598436abc10861b33b7ea97a8458d6a78a3e204 /doc | |
| parent | 68b576a178c057a016c7d4be1b319cc8fcbfac25 (diff) | |
| parent | 0900b007973759a0fea20c0395e40c6f34bed8dc (diff) | |
Merge PR #7331: Fix a typo in the reference manual: <; -> <:
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 3f4fbbd6f..a93e9b156 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -874,7 +874,7 @@ In the syntax of module application, the ! prefix indicates that any Starts an interactive module satisfying each `module_type`. - .. cmdv:: Module @ident {* @module_binding} <: {+<; @module_type }. + .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type }. Starts an interactive functor with parameters given by the list of `module_binding`. The output module type is verified against each `module_type`. |