diff options
| author | Maxime Dénès | 2017-09-07 12:46:12 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-07 12:46:12 +0200 |
| commit | 7034b1188bba2c41de87ce980f5ecfab9d2220f3 (patch) | |
| tree | c2e66295f871471bdd6f0070ea843246abc90338 /API/API.mli | |
| parent | 084ef41c98d52078f85831c940d0a073a4ccdb7a (diff) | |
| parent | 37b81fe10d2da12180d96d931ba2b76370e1eea5 (diff) | |
Merge PR #931: Parametrize module body
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/API/API.mli b/API/API.mli index fce319fe37..8b0bef48c9 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1280,23 +1280,28 @@ 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; mod_delta : Mod_subst.delta_resolver; - mod_retroknowledge : Retroknowledge.action list + mod_retroknowledge : 'a module_retroknowledge; } 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 | SFBmind of mutual_inductive_body | SFBmodule of module_body | SFBmodtype of module_type_body + and _ module_retroknowledge = + | ModBodyRK : + Retroknowledge.action list -> module_implementation module_retroknowledge + | ModTypeRK : unit module_retroknowledge end module Declareops : |