diff options
| author | Pierre-Marie Pédrot | 2017-07-28 11:41:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-29 17:24:02 +0200 |
| commit | 1974816aca996fe3ee9420b83f11d15923e70fda (patch) | |
| tree | 8b43583d6e6473dbd06a17ac7b24df3d05ba63bb /API | |
| parent | a980d38681f7ab9bfd8a180f2252ce573e3ff211 (diff) | |
Separating the module_type and module_body types by using a type parameter.
As explained in edf85b9, the original commit that merged the module_body
and module_type_body representations, this was delayed to a later time
assumedly due to OCaml lack of GADTs. Actually, the only thing that was
needed was polymorphic recursion, which has been around already for a
relatively long time (since 3.12).
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/API/API.mli b/API/API.mli index d1774afe54..aa7f93bb25 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1280,9 +1280,9 @@ sig | Algebraic of module_expression | Struct of module_signature | FullStruct - and module_body = + and 'a generic_module_body = { mod_mp : Names.ModPath.t; - mod_expr : module_implementation; + mod_expr : 'a; mod_type : module_signature; mod_type_alg : module_expression option; mod_constraints : Univ.ContextSet.t; @@ -1290,7 +1290,8 @@ sig mod_retroknowledge : Retroknowledge.action list } and module_signature = (module_type_body,structure_body) functorize - and module_type_body = module_body + and module_body = module_implementation generic_module_body + and module_type_body = unit generic_module_body and structure_body = (Names.Label.t * structure_field_body) list and structure_field_body = | SFBconst of constant_body |