1 files changed, 18 insertions, 26 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 927278965..09f7bd75c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -60,6 +60,7 @@
 open Util
 open Names
 open Declarations
+open Context.Named.Declaration
 
 (** {6 Safe environments }
 
@@ -179,20 +180,17 @@ let set_engagement c senv =
     env = Environ.set_engagement c senv.env;
     engagement = Some c }
 
+let set_typing_flags c senv =
+  { senv with env = Environ.set_typing_flags c senv.env }
+
 (** Check that the engagement [c] expected by a library matches
     the current (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."
+        CErrors.error "Needs option -impredicative-set."
     | _ -> ()
   end
 
@@ -222,13 +220,6 @@ let inline_private_constants_in_constr = Term_typing.inline_side_effects
 let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
 let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
 
-let constant_entry_of_private_constant = function
-  | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
-      [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ]
-  | { Entries.eff = Entries.SEscheme (l,_) } ->
-      List.map (fun (_,kn,cb,eff_env) ->
-        kn, Term_typing.constant_entry_of_side_effect cb eff_env) l
-
 let private_con_of_con env c =
   let cbo = Environ.lookup_constant c env.env in
   { Entries.from_env = CEphemeron.create env.revstruct;
@@ -353,10 +344,10 @@ let check_required current_libs needed =
     try
       let actual = DPMap.find id current_libs in
       if not(digest_match ~actual ~required) then
-        Errors.error
+        CErrors.error
           ("Inconsistent assumptions over module "^(DirPath.to_string id)^".")
     with Not_found ->
-      Errors.error ("Reference to unknown module "^(DirPath.to_string id)^".")
+      CErrors.error ("Reference to unknown module "^(DirPath.to_string id)^".")
   in
   Array.iter check needed
 
@@ -369,11 +360,12 @@ let check_required current_libs needed =
     hypothesis many many times, and the check performed here would
     cost too much. *)
 
-let safe_push_named (id,_,_ as d) env =
+let safe_push_named d env =
+  let id = get_id d in
   let _ =
     try
       let _ = Environ.lookup_named id env in
-      Errors.error ("Identifier "^Id.to_string id^" already defined.")
+      CErrors.error ("Identifier "^Id.to_string id^" already defined.")
     with Not_found -> () in
   Environ.push_named d env
 
@@ -390,13 +382,13 @@ let push_named_def (id,de) senv =
 	(Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o)
     | _ -> assert false in
   let senv' = push_context_set poly univs senv in
-  let env'' = safe_push_named (id,Some c,typ) senv'.env in
+  let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in
     univs, {senv' with env=env''}
 
 let push_named_assum ((id,t,poly),ctx) senv =
   let senv' = push_context_set poly ctx senv in
   let t = Term_typing.translate_local_assum senv'.env t in
-  let env'' = safe_push_named (id,None,t) senv'.env in
+  let env'' = safe_push_named (LocalAssum (id,t)) senv'.env in
     {senv' with env=env''}
 
 
@@ -823,8 +815,8 @@ let export ?except senv dir =
   let senv =
     try join_safe_environment ?except senv
     with e ->
-      let e = Errors.push e in
-      Errors.errorlabstrm "export" (Errors.iprint e)
+      let e = CErrors.push e in
+      CErrors.errorlabstrm "export" (CErrors.iprint e)
   in
   assert(senv.future_cst = []);
   let () = check_current_library dir senv in
@@ -860,7 +852,7 @@ let import lib cst vodigest senv =
   check_required senv.required lib.comp_deps;
   check_engagement senv.env lib.comp_enga;
   if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then
-    Errors.errorlabstrm "Safe_typing.import"
+    CErrors.errorlabstrm "Safe_typing.import"
      (Pp.strbrk "Cannot load a library with the same name as the current one.");
   let mp = MPfile lib.comp_name in
   let mb = lib.comp_mod in
@@ -911,7 +903,7 @@ let register_inline kn senv =
   let open Environ in
   let open Pre_env in
   if not (evaluable_constant kn senv.env) then
-    Errors.error "Register inline: an evaluable constant is expected";
+    CErrors.error "Register inline: an evaluable constant is expected";
   let env = pre_env senv.env in
   let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in
   let cb = {cb with const_inline_code = true} in