aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Kazuhiko Sakaguchi <sakaguchi@coins.tsukuba.ac.jp>2018-04-23 09:20:02 +0900
committerGravatar GitHub <noreply@github.com>2018-04-23 09:20:02 +0900
commit0900b007973759a0fea20c0395e40c6f34bed8dc (patch)
treea9e95a528057a70a327916d9ca8e94507bc44f71 /doc
parentdfbf22a098e8e2890d2e10da5d669d9960ef6771 (diff)
Fix a typo in the reference manual: <; -> <:
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/language/gallina-extensions.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 1a7628d89..2c06c237d 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`.