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.

9 files changed, 20 insertions, 44 deletions

diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index a63705adc..f196746a5 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -23,16 +23,11 @@ let print_memory_stat () =
 
 let output_context = ref false
 
-let pr_engagement (impr_set,type_in_type) =
+let pr_engagement impr_set =
   begin
     match impr_set with
     | ImpredicativeSet -> str "Theory: Set is impredicative"
     | PredicativeSet -> str "Theory: Set is predicative"
-  end ++ fnl() ++
-  begin
-    match type_in_type with
-    | StratifiedType -> str "Theory: Stratified type hierarchy"
-    | TypeInType -> str "Theory: Type is of type Type"
   end
 
 let cst_filter f csts =
diff --git a/checker/checker.ml b/checker/checker.ml
index 9d76fb09e..2c872f272 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -140,9 +140,7 @@ let set_debug () = Flags.debug := true
 
 let impredicative_set = ref Cic.PredicativeSet
 let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet
-let type_in_type = ref Cic.StratifiedType
-let set_type_in_type () = type_in_type := Cic.TypeInType
-let engage () = Safe_typing.set_engagement (!impredicative_set,!type_in_type)
+let engage () = Safe_typing.set_engagement (!impredicative_set)
 
 
 let admit_list = ref ([] : section_path list)
@@ -192,7 +190,6 @@ let print_usage_channel co command =
 \n  -silent                disable trace of constants being checked\
 \n\
 \n  -impredicative-set     set sort Set impredicative\
-\n  -type-in-type          collapse type hierarchy\
 \n\
 \n  -h, --help             print this list of options\
 \n"
@@ -313,8 +310,6 @@ let parse_args argv =
     | [] -> ()
     | "-impredicative-set" :: rem ->
       set_impredicative_set (); parse rem
-    | "-type-in-type" :: rem ->
-      set_type_in_type (); parse rem
 
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then 
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 } *)
diff --git a/checker/environ.ml b/checker/environ.ml
index 9352f71ef..881284eda 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -33,26 +33,21 @@ let empty_env = {
   env_rel_context = [];
   env_stratification =
   { env_universes = Univ.initial_universes;
-    env_engagement = (PredicativeSet,StratifiedType)};
+    env_engagement = PredicativeSet };
   env_imports = MPmap.empty }
 
 let engagement env = env.env_stratification.env_engagement
 let universes env = env.env_stratification.env_universes
 let rel_context env = env.env_rel_context
 
-let set_engagement (impr_set,type_in_type as c) env =
-  let expected_impr_set,expected_type_in_type =
+let set_engagement (impr_set as c) env =
+  let expected_impr_set =
     env.env_stratification.env_engagement in
   begin
     match impr_set,expected_impr_set with
     | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement"
     | _ -> ()
   end;
-  begin
-    match type_in_type,expected_type_in_type with
-    | StratifiedType, TypeInType -> error "Incompatible engagement"
-    | _ -> ()
-  end;
   { env with env_stratification =
       { env.env_stratification with env_engagement = c } }
 
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index a667bb8a3..29b16392b 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -176,7 +176,7 @@ let typecheck_arity env params inds =
 (* Allowed eliminations *)
 
 let check_predicativity env s small level =
-  match s, fst (engagement env) with
+  match s, engagement env with
       Type u, _ ->
         (* let u' = fresh_local_univ () in *)
         (* let cst = *)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index f1aa5d919..b280df54a 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -167,8 +167,9 @@ let sort_cmp env univ pb s0 s1 =
             CUMUL -> ()
           | _ -> raise NotConvertible)
     | (Type u1, Type u2) ->
-        if snd (engagement env) == StratifiedType
-          && not
+        (** FIXME: handle type-in-type option here *)
+        if (* snd (engagement env) == StratifiedType && *)
+          not
 	  (match pb with
             | CONV -> Univ.check_eq univ u1 u2
 	    | CUMUL -> Univ.check_leq univ u1 u2)
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 *)
 
diff --git a/checker/typeops.ml b/checker/typeops.ml
index da9842a8d..0c7e538be 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -128,7 +128,7 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        if fst (engagement env) = ImpredicativeSet then
+        if engagement env = ImpredicativeSet then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
         else
diff --git a/checker/values.ml b/checker/values.ml
index dd29f6fbe..c175aed68 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 7d7963269852d32324e10aa77beb938d  checker/cic.mli
+MD5 6466d8cc443b5896cb905776df0cc49e  checker/cic.mli
 
 *)
 
@@ -194,8 +194,7 @@ let v_lazy_constr =
 (** kernel/declarations *)
 
 let v_impredicative_set = v_enum "impr-set" 2
-let v_type_in_type = v_enum "type-in-type" 2
-let v_engagement = v_tuple "eng" [|v_impredicative_set; v_type_in_type|]
+let v_engagement = v_impredicative_set
 
 let v_pol_arity =
   v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
@@ -214,7 +213,7 @@ let v_projbody =
 	    v_constr|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool|]
+  v_tuple "typing_flags" [|v_bool; v_bool|]
 
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
@@ -275,7 +274,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     v_bool;
     v_context;
     Opt v_bool;
-    v_bool|]
+    v_typing_flags|]
 
 let v_with =
   Sum ("with_declaration_body",0,