From 1974816aca996fe3ee9420b83f11d15923e70fda Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 28 Jul 2017 11:41:25 +0200 Subject: 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). --- kernel/declareops.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/declareops.mli') diff --git a/kernel/declareops.mli b/kernel/declareops.mli index a8ba5fa39..b2d29759d 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -78,3 +78,4 @@ val safe_flags : typing_flags val hcons_const_body : constant_body -> constant_body val hcons_mind : mutual_inductive_body -> mutual_inductive_body val hcons_module_body : module_body -> module_body +val hcons_module_type : module_type_body -> module_type_body -- cgit v1.2.3