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, 7 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 469cf8d4c..364558755 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -167,9 +167,8 @@ type action
 (** Engagements *)
 
 type set_predicativity = ImpredicativeSet | PredicativeSet
-type type_hierarchy = TypeInType | StratifiedType
 
-type engagement = set_predicativity * type_hierarchy
+type engagement = set_predicativity
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
@@ -219,6 +218,7 @@ type constant_universes = Univ.universe_context
 type typing_flags = {
   check_guarded : bool; (** If [false] then fixed points and co-fixed
                             points are assumed to be total. *)
+  check_universes : bool; (** If [false] universe constraints are not checked *)
 }
 
 type constant_body = {
@@ -327,11 +327,7 @@ type mutual_inductive_body = {
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
-    mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker.  *)
-
-(** {8 Data for native compilation } *)
-
-    mind_native_name : native_name ref; (** status of the code (linked or not, and where) *)
+    mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *)
   }
 
 (** {6 Module declarations } *)