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).
---
 API/API.mli | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index d1774afe54..aa7f93bb25 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1280,9 +1280,9 @@ 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;
@@ -1290,7 +1290,8 @@ sig
                          mod_retroknowledge : Retroknowledge.action list
                        }
    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
-- 
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.

---
 API/API.mli | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index aa7f93bb25..2a60cd54a9 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1287,7 +1287,7 @@ sig
                          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_body = module_implementation generic_module_body
@@ -1298,6 +1298,10 @@ sig
                             | 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 :
-- 
cgit v1.2.3