diff options
| author | Pierre-Marie Pédrot | 2020-04-30 14:10:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-30 14:10:16 +0200 |
| commit | d436c45a19de2f91aad94f492b547225f8c5b305 (patch) | |
| tree | b666e829b6545ba38170dcf79276714dd89cbe32 /kernel/mod_typing.mli | |
| parent | 010ef152611977770fa137ed5980205d412febe5 (diff) | |
| parent | 7a4e7dfbaa8dc3fa92931c4bfa39d268940e08f8 (diff) | |
Merge PR #12107: Remove mod_constraints field of module body
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/mod_typing.mli')
| -rw-r--r-- | kernel/mod_typing.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index fd5421aefe..94a4b17df3 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -23,13 +23,13 @@ open Names *) val translate_module : - env -> ModPath.t -> inline -> module_entry -> module_body + env -> ModPath.t -> inline -> module_entry -> module_body * Univ.Constraint.t (** [translate_modtype] produces a [module_type_body] whose [mod_type_alg] cannot be [None] (and of course [mod_expr] is [Abstract]). *) val translate_modtype : - env -> ModPath.t -> inline -> module_type_entry -> module_type_body + env -> ModPath.t -> inline -> module_type_entry -> module_type_body * Univ.Constraint.t (** Low-level function for translating a module struct entry : - We translate to a module when a [ModPath.t] is given, @@ -39,7 +39,7 @@ val translate_modtype : the extraction. *) type 'alg translation = - module_signature * 'alg * delta_resolver * Univ.ContextSet.t + module_signature * 'alg * delta_resolver * Univ.Constraint.t val translate_mse : env -> ModPath.t option -> inline -> module_struct_entry -> @@ -51,7 +51,7 @@ val translate_mse : val finalize_module : env -> ModPath.t -> (module_expression option) translation -> (module_type_entry * inline) option -> - module_body + module_body * Univ.Constraint.t (** [translate_mse_incl] translate the mse of a module or module type given to an Include *) |