Fixing the checker.

I had to remove code handling the -type-in-type option introduced by commit
9c732a5. We should fix it at some point, but I am not sure that using the
checker with a system known to be blatantly inconsistent makes much sense
anyway.

1 files changed, 3 insertions, 8 deletions

diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 1071e2f93..e644febe4 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -35,20 +35,15 @@ let full_add_module dp mb univs digest =
   genv := add_digest env dp digest
 
 (* 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
+let check_engagement env expected_impredicative_set =
+  let impredicative_set = 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 *)