diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-28 11:41:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-29 17:24:02 +0200 |
| commit | 1974816aca996fe3ee9420b83f11d15923e70fda (patch) | |
| tree | 8b43583d6e6473dbd06a17ac7b24df3d05ba63bb /plugins/extraction | |
| 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 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 89c2a0ae3..f503c572d 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -281,7 +281,8 @@ and extract_msignature_spec env mp1 reso = function MTfunsig (mbid, extract_mbody_spec env mp mtb, extract_msignature_spec env' mp1 reso me) -and extract_mbody_spec env mp mb = match mb.mod_type_alg with +and extract_mbody_spec : 'a. _ -> _ -> 'a generic_module_body -> _ = + fun env mp mb -> match mb.mod_type_alg with | Some ty -> extract_mexpression_spec env mp (mb.mod_type,ty) | None -> extract_msignature_spec env mp mb.mod_delta mb.mod_type |