diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/parsetree.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/parsetree.mli b/parsing/parsetree.mli index 017bede876..e806a16091 100644 --- a/parsing/parsetree.mli +++ b/parsing/parsetree.mli @@ -804,6 +804,7 @@ and module_substitution = pms_attributes: attributes; (* ... [@@id1] [@@id2] *) pms_loc: Location.t; } +(* S := M *) and module_type_declaration = { |