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/safe_typing.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 04051f2e23..aa26405f76 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -574,7 +574,7 @@ let add_mind dir l mie senv =
 let add_modtype l params_mte inl senv =
   let mp = MPdot(senv.modpath, l) in
   let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte  in
-  let mtb = Declareops.hcons_module_body mtb in
+  let mtb = Declareops.hcons_module_type mtb in
   let senv' = add_field (l,SFBmodtype mtb) MT senv in
   mp, senv'
 
@@ -732,7 +732,7 @@ let end_module l restype senv =
 
 let build_mtb mp sign cst delta =
   { mod_mp = mp;
-    mod_expr = Abstract;
+    mod_expr = ();
     mod_type = sign;
     mod_type_alg = None;
     mod_constraints = cst;
-- 
cgit v1.2.3


From 37b81fe10d2da12180d96d931ba2b76370e1eea5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Jul 2017 14:23:37 +0200
Subject: Statically enforcing that module types have no retroknowledge.

---
 kernel/safe_typing.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index aa26405f76..ad622b07d8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -677,7 +677,7 @@ let build_module_body params restype senv =
       (struc,None,senv.modresolver,senv.univ) restype'
   in
   let mb' = functorize_module params mb in
-  { mb' with mod_retroknowledge = senv.local_retroknowledge }
+  { mb' with mod_retroknowledge = ModBodyRK senv.local_retroknowledge }
 
 (** Returning back to the old pre-interactive-module environment,
     with one extra component and some updated fields
@@ -737,7 +737,7 @@ let build_mtb mp sign cst delta =
     mod_type_alg = None;
     mod_constraints = cst;
     mod_delta = delta;
-    mod_retroknowledge = [] }
+    mod_retroknowledge = ModTypeRK }
 
 let end_modtype l senv =
   let mp = senv.modpath in
@@ -853,7 +853,7 @@ let export ?except senv dir =
       mod_type_alg = None;
       mod_constraints = senv.univ;
       mod_delta = senv.modresolver;
-      mod_retroknowledge = senv.local_retroknowledge
+      mod_retroknowledge = ModBodyRK senv.local_retroknowledge
     }
   in
   let ast, symbols =
-- 
cgit v1.2.3