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

---
 checker/modops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'checker/modops.ml')

diff --git a/checker/modops.ml b/checker/modops.ml
index 726988752..f0abc39ea 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -49,7 +49,7 @@ let destr_functor = function
   | NoFunctor _ -> error_not_a_functor ()
 
 let module_body_of_type mp mtb =
-  { mtb with mod_mp = mp; mod_expr = Abstract }
+  { mtb with mod_mp = mp; mod_expr = Abstract; mod_retroknowledge = ModBodyRK [] }
 
 let rec add_structure mp sign resolver env =
   let add_one env (l,elem) =
@@ -142,7 +142,7 @@ let module_type_of_module mp mb =
     { mb with
       mod_expr = ();
       mod_type_alg = None;
-      mod_retroknowledge = [] }
+      mod_retroknowledge = ModTypeRK }
   in
   match mp with
   | Some mp -> strengthen {mtb with mod_mp = mp} mp
-- 
cgit v1.2.3