1 files changed, 19 insertions, 11 deletions
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 810d6e0b..81a3cc03 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -27,18 +27,26 @@ let set_engagement c =
 (* full_add_module adds module with universes and constraints *)
 let full_add_module dp mb univs digest =
   let env = !genv in
-  let env = add_constraints mb.mod_constraints env in
-  let env = add_constraints univs env in
+  let env = push_context_set ~strict:true mb.mod_constraints env in
+  let env = push_context_set ~strict:true univs env in
   let env = Modops.add_module mb env in
   genv := add_digest env dp digest
 
-(* Check that the engagement expected by a library matches the initial one *)
-let check_engagement env c =
-  match engagement env, c with
-    | Some ImpredicativeSet, Some ImpredicativeSet -> ()
-    | _, None -> ()
-    | _, Some ImpredicativeSet ->
-        error "Needs option -impredicative-set"
+(* Check that the engagement expected by a library extends the initial one *)
+let check_engagement env (expected_impredicative_set,expected_type_in_type) =
+  let impredicative_set,type_in_type = Environ.engagement env in
+  begin
+    match impredicative_set, expected_impredicative_set with
+    | PredicativeSet, ImpredicativeSet ->
+        Errors.error "Needs option -impredicative-set."
+    | _ -> ()
+  end;
+  begin
+    match type_in_type, expected_type_in_type with
+    | StratifiedType, TypeInType ->
+        Errors.error "Needs option -type-in-type."
+    | _ -> ()
+  end
 
 (* Libraries = Compiled modules *)
 
@@ -75,8 +83,8 @@ let import file clib univs digest =
   check_engagement env clib.comp_enga;
   let mb = clib.comp_mod in
   Mod_checking.check_module
-    (add_constraints univs
-      (add_constraints mb.mod_constraints env)) mb.mod_mp mb;
+    (push_context_set ~strict:true univs
+      (push_context_set ~strict:true mb.mod_constraints env)) mb.mod_mp mb;
   stamp_library file digest;
   full_add_module clib.comp_name mb univs digest