diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b4f7abbb0b..fdf73d047d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -343,7 +343,8 @@ GEXTEND Gram [ [ bls = LIST0 module_binders -> List.flatten bls ] ] ; of_module_type: - [ [ ":"; mty = Module.module_type -> mty ] ] + [ [ ":"; mty = Module.module_type -> (mty, true) + | "<:"; mty = Module.module_type -> (mty, false) ] ] ; is_module_type: [ [ ":="; mty = Module.module_type -> mty ] ] |