diff options
| author | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
| commit | c70412ec8b0bb34b7a5607c07d34607a147d834c (patch) | |
| tree | 0cc6cd76a8f70dfd2f5b55b0db96db4de2ff07a2 /kernel/modops.mli | |
| parent | 720ee2730684cc289cef588482323d177e0bea59 (diff) | |
| parent | 191e253d1d1ebd6c76c63b3d83f4228e46196a6e (diff) | |
Merge PR #6914: Primitive integers
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'kernel/modops.mli')
| -rw-r--r-- | kernel/modops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli index 0acd09fb12..bb97f0171e 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -57,6 +57,8 @@ val add_linked_module : module_body -> link_info -> env -> env (** same, for a module type *) val add_module_type : ModPath.t -> module_type_body -> env -> env +val add_retroknowledge : module_implementation module_retroknowledge -> env -> env + (** {6 Strengthening } *) val strengthen : module_type_body -> ModPath.t -> module_type_body |