Imported Upstream version 8.6upstream/8.6

24 files changed, 352 insertions, 360 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 3a5c9121..8b299bf2 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -7,10 +7,12 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 
+let chk_pp = Pp.pp_with Format.std_formatter
+
 let pr_dirpath dp = str (DirPath.to_string dp)
 let default_root_prefix = DirPath.empty
 let split_dirpath d =
@@ -111,15 +113,13 @@ let check_one_lib admit (dir,m) =
      also check if it carries a validation certificate (yet to
      be implemented). *)
   if LibrarySet.mem dir admit then
-    (Flags.if_verbose ppnl
+    (Flags.if_verbose Feedback.msg_notice
       (str "Admitting library: " ++ pr_dirpath dir);
       Safe_typing.unsafe_import file md m.library_extra_univs dig)
   else
-    (Flags.if_verbose ppnl
+    (Flags.if_verbose Feedback.msg_notice
       (str "Checking library: " ++ pr_dirpath dir);
       Safe_typing.import file md m.library_extra_univs dig);
-  Flags.if_verbose pp (fnl());
-  pp_flush ();
   register_loaded_library m
 
 (*************************************************************************)
@@ -173,7 +173,7 @@ let remove_load_path dir =
 
 let add_load_path (phys_path,coq_path) =
   if !Flags.debug then
-    ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
+    Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
            str phys_path);
   let phys_path = canonical_path_name phys_path in
   let physical, logical = !load_paths in
@@ -188,7 +188,7 @@ let add_load_path (phys_path,coq_path) =
 	    begin
               (* Assume the user is concerned by library naming *)
 	      if dir <> default_root_prefix then
-		msg_warning
+		Feedback.msg_warning
 		  (str phys_path ++ strbrk " was previously bound to " ++
 		   pr_dirpath dir ++ strbrk "; it is remapped to " ++
 		   pr_dirpath coq_path);
@@ -299,12 +299,12 @@ let name_clash_message dir mdir f =
 let depgraph = ref LibraryMap.empty
 
 let intern_from_file (dir, f) =
-  Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
+  Flags.if_verbose chk_pp (str"[intern "++str f++str" ...");
   let (sd,md,table,opaque_csts,digest) =
     try
       let ch = System.with_magic_number_check raw_intern_library f in
       let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in
-      let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in
+      let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
       let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in
       let (discharging:'a option), _, _ = System.marshal_in_segment f ch in
       let (tasks:'a option), _, _ = System.marshal_in_segment f ch in
@@ -323,7 +323,7 @@ let intern_from_file (dir, f) =
         errorlabstrm "intern_from_file"
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
-        pp (str " (was a vio file) ");
+       chk_pp (str " (was a vio file) ");
       Option.iter (fun (_,_,b) -> if not b then
         errorlabstrm "intern_from_file"
           (str "The file "++str f++str " is still a .vio"))
@@ -334,12 +334,12 @@ let intern_from_file (dir, f) =
       Validate.validate !Flags.debug Values.v_libsum sd;
       Validate.validate !Flags.debug Values.v_lib md;
       Validate.validate !Flags.debug Values.v_opaques table;
-      Flags.if_verbose ppnl (str" done]"); pp_flush ();
+      Flags.if_verbose chk_pp (str" done]" ++ fnl ());
       let digest =
         if opaque_csts <> None then Cic.Dviovo (digest,udg)
         else (Cic.Dvo digest) in
       sd,md,table,opaque_csts,digest
-    with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
+    with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in
   depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
   opaque_tables := LibraryMap.add sd.md_name table !opaque_tables;
   Option.iter (fun (opaque_csts,_,_) ->
@@ -407,11 +407,11 @@ let recheck_library ~norec ~admit ~check =
   let nochk =
     List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in
   (* *)
-  Flags.if_verbose ppnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
+  Flags.if_verbose Feedback.msg_notice (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
     prlist
     (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
   List.iter (check_one_lib nochk) needed;
-  Flags.if_verbose ppnl (str"Modules were successfully checked")
+  Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked")
 
 open Printf
 
diff --git a/checker/check.mllib b/checker/check.mllib
index 0d36e3a0..488507a1 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -8,6 +8,7 @@ Hashcons
 CSet
 CMap
 Int
+Dyn
 HMap
 Option
 Store
@@ -21,20 +22,25 @@ CList
 CString
 Serialize
 Stateid
-Feedback
-Pp
-Segmenttree
-Unicodetable
-Unicode
 CObj
 CArray
 CStack
 Util
+Pp
 Ppstyle
-Errors
-Ephemeron
+Xml_datatype
+Richpp
+Feedback
+Segmenttree
+Unicodetable
+Unicode
+CErrors
+CWarnings
+CEphemeron
 Future
 CUnix
+
+Minisys
 System
 Profile
 RemoteCounter
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index d031975d..741f5328 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -18,21 +18,16 @@ let print_memory_stat () =
   if !memory_stat then begin
     Format.printf "total heap size = %d kbytes\n" (CObj.heap_size_kb ());
     Format.print_newline();
-    flush_all()
+    Format.print_flush()
   end
 
 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 ++
-  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 =
@@ -57,12 +52,12 @@ let print_context env =
          env_modules=mods; env_modtypes=mtys};
        env_stratification=
         {env_universes=univ; env_engagement=engt}} = env in
-    ppnl(hov 0
+    Feedback.msg_notice
+      (hov 0
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
       str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
-      str "* " ++ hov 0 (pr_ax csts) ++
-      fnl())); pp_flush()
+      str "* " ++ hov 0 (pr_ax csts)));
   end
 
 let stats () =
diff --git a/checker/checker.ml b/checker/checker.ml
index 825fb4dc..8dbb7e01 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open System
 open Flags
@@ -16,8 +16,10 @@ open Check
 
 let () = at_exit flush_all
 
+let chk_pp = Pp.pp_with Format.std_formatter
+
 let fatal_error info anomaly =
-  flush_all (); pperrnl info; flush_all ();
+  flush_all (); Feedback.msg_error info; flush_all ();
   exit (if anomaly then 129 else 1)
 
 let coq_root = Id.of_string "Coq"
@@ -67,12 +69,12 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
       Check.add_load_path (dir,coq_dirpath)
     end
   else
-    msg_warning (str "Cannot open " ++ str dir)
+    Feedback.msg_warning (str "Cannot open " ++ str dir)
 
 let convert_string d =
   try Id.of_string d
-  with Errors.UserError _ ->
-    if_verbose msg_warning
+  with CErrors.UserError _ ->
+    if_verbose Feedback.msg_warning
       (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
     raise Exit
 
@@ -90,7 +92,7 @@ let add_rec_path ~unix_path ~coq_root =
     List.iter Check.add_load_path dirs;
     Check.add_load_path (unix_path, coq_root)
   else
-    msg_warning (str "Cannot open " ++ str unix_path)
+    Feedback.msg_warning (str "Cannot open " ++ str unix_path)
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
@@ -123,7 +125,7 @@ let init_load_path () =
     add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
   (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
   List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix)
-    (xdg_dirs ~warn:(fun x -> msg_warning (str x)));
+    (xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)));
   (* then directories in COQPATH *)
   List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath;
   (* then current directory *)
@@ -140,9 +142,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)
@@ -179,10 +179,7 @@ let print_usage_channel co command =
   output_string co command;
   output_string co "coqchk options are:\n";
   output_string co
-"  -I dir -as coqdir      map physical dir to logical coqdir\
-\n  -I dir                 map directory dir to the empty logical path\
-\n  -include dir           (idem)\
-\n  -R dir coqdir          recursively map physical dir to logical coqdir\
+"  -R dir coqdir          map physical dir to logical coqdir\
 \n\
 \n  -admit module          load module and dependencies without checking\
 \n  -norec module          check module but admit dependencies without checking\
@@ -195,7 +192,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"
@@ -215,14 +211,9 @@ let usage () =
 open Type_errors
 
 let anomaly_string () = str "Anomaly: "
-let report () = (str "." ++ spc () ++ str "Please report.")
+let report () = (str "." ++ spc () ++ str "Please report" ++
+                 strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".")
 
-let print_loc loc =
-  if loc = Loc.ghost then
-    (str"<unknown>")
-  else
-    let loc = Loc.unloc loc in
-    (int (fst loc) ++ str"-" ++ int (snd loc))
 let guill s = str "\"" ++ str s ++ str "\""
 
 let where s =
@@ -294,7 +285,8 @@ let rec explain_exn = function
           Format.printf "@\nis not convertible with@\n";
           Print.print_pure_constr a;
           Format.printf "@\n====== universes ====@\n";
-          Pp.pp (Univ.pr_universes
+          chk_pp
+            (Univ.pr_universes
             (ctx.Environ.env_stratification.Environ.env_universes));
           str "\nCantApplyBadType at argument " ++ int n
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
@@ -315,15 +307,13 @@ let rec explain_exn = function
 		   str ", characters " ++ int e ++ str "-" ++
 		   int (e+6) ++ str ")")) ++
 	       report ())
-  | e -> Errors.print e (* for anomalies and other uncaught exceptions *)
+  | e -> CErrors.print e (* for anomalies and other uncaught exceptions *)
 
 let parse_args argv =
   let rec parse = function
     | [] -> ()
     | "-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 
@@ -337,15 +327,13 @@ let parse_args argv =
     | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
 
-    | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem
-    | "-R" :: d :: "-as" :: [] -> usage ()
     | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem
     | "-R" :: ([] | [_]) -> usage ()
 
     | "-debug" :: rem -> set_debug (); parse rem
 
     | "-where" :: _ ->
-        Envars.set_coqlib ~fail:Errors.error;
+        Envars.set_coqlib ~fail:CErrors.error;
         print_endline (Envars.coqlib ());
         exit 0
 
@@ -383,7 +371,7 @@ let init_with_argv argv =
     try
       parse_args argv;
       if !Flags.debug then Printexc.record_backtrace true;
-      Envars.set_coqlib ~fail:Errors.error;
+      Envars.set_coqlib ~fail:CErrors.error;
       if_verbose print_header ();
       init_load_path ();
       engage ();
diff --git a/checker/cic.mli b/checker/cic.mli
index 041394d4..36455875 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -111,7 +111,8 @@ type cofixpoint = constr pcofixpoint
 
 (** {6 Type of assumptions and contexts}  *)
 
-type rel_declaration = Name.t * constr option * constr
+type rel_declaration = LocalAssum of Name.t * constr          (* name, type *)
+                     | LocalDef of Name.t * constr * constr   (* name, value, type *)
 type rel_context = rel_declaration list
 
 (** The declarations below in .vo should be outside sections,
@@ -166,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) } *)
 
@@ -211,6 +211,16 @@ type constant_def =
 
 type constant_universes = Univ.universe_context
 
+(** The [typing_flags] are instructions to the type-checker which
+    modify its behaviour. The typing flags used in the type-checking
+    of a constant are tracked in their {!constant_body} so that they
+    can be displayed to the user. *)
+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 = {
     const_hyps : section_context; (** New: younger hyp at top *)
     const_body : constant_def;
@@ -219,7 +229,9 @@ type constant_body = {
     const_polymorphic : bool; (** Is it polymorphic or not *)
     const_universes : constant_universes;
     const_proj : projection_body option;
-    const_inline_code : bool }
+    const_inline_code : bool;
+    const_typing_flags : typing_flags;
+}
 
 (** {6 Representation of mutual inductive types } *)
 
@@ -315,9 +327,7 @@ type mutual_inductive_body = {
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
-(** {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/closure.ml b/checker/closure.ml
index 400a535c..cef1d31a 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -29,7 +29,7 @@ let reset () =
   beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0
 
 let stop() =
-  msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
+  Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
 	 str" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++
          str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]")
 
@@ -217,10 +217,10 @@ let ref_value_cache info ref =
 let defined_rels flags env =
 (*  if red_local_const (snd flags) then*)
   fold_rel_context
-      (fun (id,b,t) (i,subs) ->
-	 match b with
-	   | None -> (i+1, subs)
-	   | Some body -> (i+1, (i,body) :: subs))
+      (fun decl (i,subs) ->
+	 match decl with
+	   | LocalAssum _ -> (i+1, subs)
+	   | LocalDef (_,body,_) -> (i+1, (i,body) :: subs))
       (rel_context env) ~init:(0,[])
 (*  else (0,[])*)
 
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 32d1713a..1fe02c8b 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -73,32 +73,32 @@ let solve_delta_kn resolve kn =
       | Equiv kn1 -> kn1
       | Inline _ -> raise Not_found
   with Not_found ->
-    let mp,dir,l = repr_kn kn in
+    let mp,dir,l = KerName.repr kn in
     let new_mp = find_prefix resolve mp in
     if mp == new_mp then
       kn
     else
-      make_kn new_mp dir l
+      KerName.make new_mp dir l
 
 let gen_of_delta resolve x kn fix_can =
   let new_kn = solve_delta_kn resolve kn in
   if kn == new_kn then x else fix_can new_kn
 
 let constant_of_delta resolve con =
-  let kn = user_con con in
-  gen_of_delta resolve con kn (constant_of_kn_equiv kn)
+  let kn = Constant.user con in
+  gen_of_delta resolve con kn (Constant.make kn)
 
 let constant_of_delta2 resolve con =
-  let kn, kn' = canonical_con con, user_con con in
-  gen_of_delta resolve con kn (constant_of_kn_equiv kn')
+  let kn, kn' = Constant.canonical con, Constant.user con in
+  gen_of_delta resolve con kn (Constant.make kn')
 
 let mind_of_delta resolve mind =
-  let kn = user_mind mind in
-  gen_of_delta resolve mind kn (mind_of_kn_equiv kn)
+  let kn = MutInd.user mind in
+  gen_of_delta resolve mind kn (MutInd.make kn)
 
 let mind_of_delta2 resolve mind =
-  let kn, kn' = canonical_mind mind, user_mind mind in
-  gen_of_delta resolve mind kn (mind_of_kn_equiv kn')
+  let kn, kn' = MutInd.canonical mind, MutInd.user mind in
+  gen_of_delta resolve mind kn (MutInd.make kn')
 
 let find_inline_of_delta kn resolve =
   match Deltamap.find_kn kn resolve with
@@ -106,7 +106,7 @@ let find_inline_of_delta kn resolve =
     | _ -> raise Not_found
 
 let constant_of_delta_with_inline resolve con =
-  let kn1,kn2 = canonical_con con,user_con con in
+  let kn1,kn2 = Constant.canonical con, Constant.user con in
   try find_inline_of_delta kn2 resolve
   with Not_found ->
     try find_inline_of_delta kn1 resolve
@@ -137,17 +137,17 @@ let subst_mp sub mp =
   | Some (mp',_) -> mp'
 
 let subst_kn_delta sub kn =
- let mp,dir,l = repr_kn kn in
+ let mp,dir,l = KerName.repr kn in
   match subst_mp0 sub mp with
      Some (mp',resolve) ->
-      solve_delta_kn resolve (make_kn mp' dir l)
+      solve_delta_kn resolve (KerName.make mp' dir l)
    | None -> kn
 
 let subst_kn sub kn =
- let mp,dir,l = repr_kn kn in
+ let mp,dir,l = KerName.repr kn in
   match subst_mp0 sub mp with
      Some (mp',_) ->
-      make_kn mp' dir l
+      KerName.make mp' dir l
    | None -> kn
 
 exception No_subst
@@ -165,14 +165,14 @@ let gen_subst_mp f sub mp1 mp2 =
     | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2
 
 let make_mind_equiv mpu mpc dir l =
-  let knu = make_kn mpu dir l in
-  if mpu == mpc then mind_of_kn knu
-  else mind_of_kn_equiv knu (make_kn mpc dir l)
+  let knu = KerName.make mpu dir l in
+  if mpu == mpc then MutInd.make1 knu
+  else MutInd.make knu (KerName.make mpc dir l)
 
 let subst_ind sub mind =
-  let kn1,kn2 = user_mind mind, canonical_mind mind in
-  let mp1,dir,l = repr_kn kn1 in
-  let mp2,_,_ = repr_kn kn2 in
+  let kn1,kn2 = MutInd.user mind, MutInd.canonical mind in
+  let mp1,dir,l = KerName.repr kn1 in
+  let mp2,_,_ = KerName.repr kn2 in
   let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in
   try
     let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in
@@ -182,14 +182,14 @@ let subst_ind sub mind =
   with No_subst -> mind
 
 let make_con_equiv mpu mpc dir l =
-  let knu = make_kn mpu dir l in
-  if mpu == mpc then constant_of_kn knu
-  else constant_of_kn_equiv knu (make_kn mpc dir l)
+  let knu = KerName.make mpu dir l in
+  if mpu == mpc then Constant.make1 knu
+  else Constant.make knu (KerName.make mpc dir l)
 
 let subst_con0 sub con u =
-  let kn1,kn2 = user_con con,canonical_con con in
-  let mp1,dir,l = repr_kn kn1 in
-  let mp2,_,_ = repr_kn kn2 in
+  let kn1,kn2 = Constant.user con, Constant.canonical con in
+  let mp1,dir,l = KerName.repr kn1 in
+  let mp2,_,_ = KerName.repr kn2 in
   let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in
   let dup con = con, Const (con, u) in
   let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
@@ -304,7 +304,9 @@ let subset_prefixed_by mp resolver =
     match hint with
       | Inline _ -> rslv
       | Equiv _ ->
-	if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv
+	if mp_in_mp mp (KerName.modpath kn)
+        then Deltamap.add_kn kn hint rslv
+        else rslv
   in
   Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver
 
@@ -517,11 +519,8 @@ let map_decl_arity f g = function
   | RegularArity a -> RegularArity (f a)
   | TemplateArity a -> TemplateArity (g a)
 
-
-let subst_rel_declaration sub (id,copt,t as x) =
-  let copt' = Option.smartmap (subst_mps sub) copt in
-  let t' = subst_mps sub t in
-  if copt == copt' && t == t' then x else (id,copt',t')
+let subst_rel_declaration sub =
+  Term.map_rel_decl (subst_mps sub)
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
diff --git a/checker/environ.ml b/checker/environ.ml
index f8f5c29b..7b59c6b9 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -1,4 +1,4 @@
-open Errors
+open CErrors
 open Util
 open Names
 open Cic
@@ -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 } }
 
@@ -80,7 +75,7 @@ let push_rel d env =
 let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x
 
 let push_rec_types (lna,typarray,_) env =
-  let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
+  let ctxt = Array.map2_i (fun i na t -> LocalAssum (na, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
 (* Universe constraints *)
@@ -112,7 +107,7 @@ let anomaly s = anomaly (Pp.str s)
 let add_constant kn cs env =
   if Cmap_env.mem kn env.env_globals.env_constants then
     Printf.ksprintf anomaly ("Constant %s is already defined")
-      (string_of_con kn);
+      (Constant.to_string kn);
   let new_constants =
     Cmap_env.add kn cs env.env_globals.env_constants in
   let new_globals =
@@ -172,12 +167,14 @@ let lookup_projection p env =
 let scrape_mind env kn=
   try
     KNmap.find kn env.env_globals.env_inductives_eq
-  with 
-      Not_found -> kn
+  with
+    Not_found -> kn
 
 let mind_equiv env (kn1,i1) (kn2,i2) =
   Int.equal i1 i2 &&
-  KerName.equal (scrape_mind env (user_mind kn1)) (scrape_mind env (user_mind kn2))
+  KerName.equal
+    (scrape_mind env (MutInd.user kn1))
+    (scrape_mind env (MutInd.user kn2))
 
 
 let lookup_mind kn env =
@@ -186,9 +183,9 @@ let lookup_mind kn env =
 let add_mind kn mib env =
   if Mindmap_env.mem kn env.env_globals.env_inductives then
     Printf.ksprintf anomaly ("Inductive %s is already defined")
-      (string_of_mind kn);
+      (MutInd.to_string kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
-  let kn1,kn2 =  user_mind kn,canonical_mind kn in
+  let kn1,kn2 =  MutInd.user kn, MutInd.canonical kn in
   let new_inds_eq = if KerName.equal kn1 kn2 then
     env.env_globals.env_inductives_eq
   else
@@ -205,7 +202,7 @@ let add_mind kn mib env =
 let add_modtype ln mtb env =
   if MPmap.mem ln env.env_globals.env_modtypes then
     Printf.ksprintf anomaly ("Module type %s is already defined")
-      (string_of_mp ln);
+      (ModPath.to_string ln);
   let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
   let new_globals =
     { env.env_globals with
@@ -215,7 +212,7 @@ let add_modtype ln mtb env =
 let shallow_add_module mp mb env =
   if MPmap.mem mp env.env_globals.env_modules then
     Printf.ksprintf anomaly ("Module %s is already defined")
-      (string_of_mp mp);
+      (ModPath.to_string mp);
   let new_mods = MPmap.add mp mb env.env_globals.env_modules in
   let new_globals =
     { env.env_globals with
@@ -225,7 +222,7 @@ let shallow_add_module mp mb env =
 let shallow_remove_module mp env =
   if not (MPmap.mem mp env.env_globals.env_modules) then
     Printf.ksprintf anomaly ("Module %s is unknown")
-      (string_of_mp mp);
+      (ModPath.to_string mp);
   let new_mods = MPmap.remove mp env.env_globals.env_modules in
   let new_globals =
     { env.env_globals with
diff --git a/checker/include b/checker/include
index f5bd2984..6bea3c91 100644
--- a/checker/include
+++ b/checker/include
@@ -31,7 +31,7 @@ open Typeops;;
 open Check;;
 
 open Pp;;
-open Errors;;
+open CErrors;;
 open Util;;
 open Names;;
 open Term;;
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 2865f5bd..27f79e79 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Cic
@@ -32,11 +32,11 @@ let string_of_mp mp =
   if !Flags.debug then debug_string_of_mp mp else string_of_mp mp
 
 let prkn kn =
-  let (mp,_,l) = repr_kn kn in
+  let (mp,_,l) = KerName.repr kn in
   str(string_of_mp mp ^ "." ^ Label.to_string l)
 let prcon c =
-  let ck = canonical_con c in
-  let uk = user_con c in
+  let ck = Constant.canonical c in
+  let uk = Constant.user c in
   if KerName.equal ck uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")")
 
 (* Same as noccur_between but may perform reductions.
@@ -44,7 +44,7 @@ let prcon c =
 let weaker_noccur_between env x nvars t =
   if noccur_between x nvars t then Some t
   else
-   let t' = whd_betadeltaiota env t in
+   let t' = whd_all env t in
    if noccur_between x nvars t' then Some t'
    else None
 
@@ -56,10 +56,10 @@ let is_constructor_head t =
 let conv_ctxt_prefix env (ctx1:rel_context) ctx2 =
   let rec chk env rctx1 rctx2 =
     match rctx1, rctx2 with
-        (_,None,ty1 as d1)::rctx1', (_,None,ty2)::rctx2' ->
+        (LocalAssum (_,ty1) as d1)::rctx1', LocalAssum (_,ty2)::rctx2' ->
           conv env ty1 ty2;
           chk (push_rel d1 env) rctx1' rctx2'
-      | (_,Some bd1,ty1 as d1)::rctx1', (_,Some bd2,ty2)::rctx2' ->
+      | (LocalDef (_,bd1,ty1) as d1)::rctx1', LocalDef (_,bd2,ty2)::rctx2' ->
           conv env ty1 ty2;
           conv env bd1 bd2;
           chk (push_rel d1 env) rctx1' rctx2'
@@ -90,14 +90,14 @@ exception InductiveError of inductive_error
 (* Typing the arities and constructor types *)
 
 let rec sorts_of_constr_args env t =
-  let t = whd_betadeltaiota_nolet env t in
+  let t = whd_allnolet env t in
   match t with
     | Prod (name,c1,c2) ->
         let varj = infer_type env c1 in
-	let env1 = push_rel (name,None,c1) env in
+	let env1 = push_rel (LocalAssum (name,c1)) env in
 	varj :: sorts_of_constr_args env1 c2
     | LetIn (name,def,ty,c) ->
-        let env1 = push_rel (name,Some def,ty) env in
+        let env1 = push_rel (LocalDef (name,def,ty)) env in
 	sorts_of_constr_args env1 c
     | _ when is_constructor_head t -> []
     | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor")
@@ -167,7 +167,7 @@ let typecheck_arity env params inds =
 	   full_arity is used as argument or subject to cast, an
 	   upper universe will be generated *)
 	let id = ind.mind_typename in
-	let env_ar' = push_rel (Name id, None, arity) env_ar in
+	let env_ar' = push_rel (LocalAssum (Name id, arity)) env_ar in
         env_ar')
       env
       inds in
@@ -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 = *)
@@ -319,9 +319,9 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
   let nhyps = List.length hyps in
   let rec check k index = function
     | [] -> ()
-    | (_,Some _,_)::hyps -> check k (index+1) hyps
+    | LocalDef _ :: hyps -> check k (index+1) hyps
     | _::hyps ->
-        match whd_betadeltaiota env lpar.(k) with
+        match whd_all env lpar.(k) with
 	  | Rel w when w = index -> check (k-1) (index+1) hyps
 	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l)))
   in check (nparams-1) (n-nhyps) hyps;
@@ -340,9 +340,9 @@ let check_rec_par (env,n,_,_) hyps nrecp largs =
       | ([],_) -> ()
       | (_,[]) ->
           failwith "number of recursive parameters cannot be greater than the number of parameters."
-      | (lp,(_,Some _,_)::hyps) -> find (index-1) (lp,hyps)
+      | (lp,LocalDef _ :: hyps) -> find (index-1) (lp,hyps)
       | (p::lp,_::hyps) ->
-          (match whd_betadeltaiota env p with
+          (match whd_all env p with
 	    | Rel w when w = index -> find (index-1) (lp,hyps)
             | _ -> failwith "bad number of recursive parameters")
   in find (n-1) (lpar,List.rev hyps)
@@ -370,14 +370,15 @@ let abstract_mind_lc env ntyps npars lc =
    [lra] is the list of recursive tree of each variable
  *)
 let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
- (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra)
+ (push_rel (LocalAssum (x,a)) env, n+1, ntypes, (Norec,ra)::lra)
 
 let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) =
   let auxntyp = 1 in
   let specif = lookup_mind_specif env mi in
   let env' =
-    push_rel (Anonymous,None,
-              hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) env in
+    let decl = LocalAssum (Anonymous,
+                           hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) in
+    push_rel decl env in
   let ra_env' =
     (Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
@@ -387,7 +388,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) =
 
 let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
   if n=0 then (ienv,c) else
-    let c' = whd_betadeltaiota env c in
+    let c' = whd_all env c in
     match c' with
 	Prod(na,a,b) ->
 	  let ienv' = ienv_push_var ienv (na,a,mk_norec) in
@@ -400,7 +401,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
   let lparams = rel_context_length hyps in
   (* check the inductive types occur positively in [c] *)
   let rec check_pos (env, n, ntypes, ra_env as ienv) c =
-    let x,largs = decompose_app (whd_betadeltaiota env c) in
+    let x,largs = decompose_app (whd_all env c) in
       match x with
 	| Prod (na,b,d) ->
 	    assert (List.is_empty largs);
@@ -469,7 +470,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
 
   and check_constructors ienv check_head c =
     let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c =
-      let x,largs = decompose_app (whd_betadeltaiota env c) in
+      let x,largs = decompose_app (whd_all env c) in
 	match x with
           | Prod (na,b,d) ->
 	      assert (List.is_empty largs);
@@ -527,7 +528,7 @@ let check_positivity env_ar mind params nrecp inds =
 (************************************************************************)
 
 let check_inductive env kn mib =
-  Flags.if_verbose ppnl (str "  checking ind: " ++ pr_mind kn); pp_flush ();
+  Flags.if_verbose Feedback.msg_notice (str "  checking ind: " ++ MutInd.print kn);
   (* check mind_constraints: should be consistent with env *)
   let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 79dba4fa..c4ffc141 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Cic
@@ -31,20 +31,20 @@ let lookup_mind_specif env (kn,tyi) =
   (mib, mib.mind_packets.(tyi))
 
 let find_rectype env c =
-  let (t, l) = decompose_app (whd_betadeltaiota env c) in
+  let (t, l) = decompose_app (whd_all env c) in
   match t with
   | Ind ind -> (ind, l)
   | _ -> raise Not_found
 
 let find_inductive env c =
-  let (t, l) = decompose_app (whd_betadeltaiota env c) in
+  let (t, l) = decompose_app (whd_all env c) in
   match t with
     | Ind (ind,_)
         when (fst (lookup_mind_specif env ind)).mind_finite != CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let find_coinductive env c =
-  let (t, l) = decompose_app (whd_betadeltaiota env c) in
+  let (t, l) = decompose_app (whd_all env c) in
   match t with
     | Ind (ind,_)
         when (fst (lookup_mind_specif env ind)).mind_finite == CoFinite -> (ind, l)
@@ -59,16 +59,6 @@ let inductive_instance mib =
     UContext.instance mib.mind_universes
   else Instance.empty
 
-let inductive_context mib =
-  if mib.mind_polymorphic then 
-    instantiate_univ_context mib.mind_universes 
-  else UContext.empty
-
-let instantiate_inductive_constraints mib u =
-  if mib.mind_polymorphic then
-    subst_instance_constraints u (UContext.constraints mib.mind_universes)
-  else Constraint.empty
-
 (************************************************************************)
 
 (* Build the substitution that replaces Rels by the appropriate *)
@@ -88,10 +78,10 @@ let instantiate_params full t u args sign =
     anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
   let (rem_args, subs, ty) =
     fold_rel_context
-      (fun (_,copt,_) (largs,subs,ty) ->
-        match (copt, largs, ty) with
-          | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
-          | (Some b,_,LetIn(_,_,_,t))    -> 
+      (fun decl (largs,subs,ty) ->
+        match (decl, largs, ty) with
+          | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t)
+          | (LocalDef (_,b,_),_,LetIn(_,_,_,t))    ->
 	    (largs, (substl subs (subst_instance_constr u b))::subs, t)
 	  | (_,[],_)                -> if full then fail() else ([], subs, ty)
 	  | _                       -> fail ())
@@ -161,7 +151,7 @@ let remember_subst u subst =
 (* Propagate the new levels in the signature *)
 let rec make_subst env =
   let rec make subst = function
-    | (_,Some _,_)::sign, exp, args ->
+    | LocalDef _ :: sign, exp, args ->
         make subst (sign, exp, args)
     | d::sign, None::exp, args ->
         let args = match args with _::args -> args | [] -> [] in
@@ -174,7 +164,7 @@ let rec make_subst env =
         (* a useless extra constraint *)
         let s = sort_as_univ (snd (dest_arity env a)) in
         make (cons_subst u s subst) (sign, exp, args)
-    | (na,None,t)::sign, Some u::exp, [] ->
+    | LocalAssum (na,t) :: sign, Some u::exp, [] ->
         (* No more argument here: we add the remaining universes to the *)
         (* substitution (when [u] is distinct from all other universes in the *)
         (* template, it is identity substitution  otherwise (ie. when u is *)
@@ -190,8 +180,6 @@ let rec make_subst env =
   in
   make Univ.LMap.empty
 
-exception SingletonInductiveBecomesProp of Id.t
-
 let instantiate_universes env ctx ar argsorts =
   let args = Array.to_list argsorts in
   let subst = make_subst env (ctx,ar.template_param_levels,args) in
@@ -208,11 +196,7 @@ let instantiate_universes env ctx ar argsorts =
 
 (* Type of an inductive type *)
 
-let is_prop_sort = function
-  | Prop Null -> true
-  | _ -> false
-
-let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
+let type_of_inductive_gen env ((mib,mip),u) paramtyps =
   match mip.mind_arity with
   | RegularArity a ->
     if not mib.mind_polymorphic then a.mind_user_arity
@@ -220,25 +204,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
     let ctx,s = instantiate_universes env ctx ar paramtyps in
-      (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
-         the situation where a non-Prop singleton inductive becomes Prop
-         when applied to Prop params *)
-      if not polyprop && not (Univ.is_type0m_univ ar.template_level) && is_prop_sort s
-      then raise (SingletonInductiveBecomesProp mip.mind_typename);
-      mkArity (List.rev ctx,s)
-
-let type_of_inductive env pind = 
-  type_of_inductive_gen env pind [||]
-
-let constrained_type_of_inductive env ((mib,mip),u as pind) =
-  let ty = type_of_inductive_gen env pind [||] in
-  let cst = instantiate_inductive_constraints mib u in
-    (ty, cst)
-
-let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args =
-  let ty = type_of_inductive_gen env pind args in
-  let cst = instantiate_inductive_constraints mib u in
-    (ty, cst)
+    mkArity (List.rev ctx,s)
 
 let type_of_inductive_knowing_parameters env mip args = 
   type_of_inductive_gen env mip args
@@ -275,16 +241,6 @@ let type_of_constructor_gen (cstr,u) (mib,mip as mspec) =
 let type_of_constructor cstru mspec = 
   type_of_constructor_gen cstru mspec
 
-let type_of_constructor_in_ctx cstr (mib,mip as mspec) =
-  let u = Univ.UContext.instance mib.mind_universes in
-  let c = type_of_constructor_gen (cstr, u) mspec in
-    (c, mib.mind_universes)
-
-let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) =
-  let ty = type_of_constructor_gen cstru ind in
-  let cst = instantiate_inductive_constraints mib u in
-    (ty, cst)
-
 let arities_of_specif (kn,u) (mib,mip) =
   let specif = mip.mind_nf_lc in
   Array.map (constructor_instantiate kn u mib) specif
@@ -319,8 +275,8 @@ let elim_sorts (_,mip) = mip.mind_kelim
 
 let extended_rel_list n hyps =
   let rec reln l p = function
-    | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
-    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
+    | LocalDef _ :: hyps -> reln l (p+1) hyps
     | [] -> l
   in
   reln [] 1 hyps
@@ -343,15 +299,15 @@ let check_allowed_sort ksort specif =
 let is_correct_arity env c (p,pj) ind specif params =
   let arsign,_ = get_instantiated_arity ind specif params in
   let rec srec env pt ar =
-    let pt' = whd_betadeltaiota env pt in
+    let pt' = whd_all env pt in
     match pt', ar with
-      | Prod (na1,a1,t), (_,None,a1')::ar' ->
+      | Prod (na1,a1,t), LocalAssum (_,a1')::ar' ->
           (try conv env a1 a1'
           with NotConvertible -> raise (LocalArity None));
-          srec (push_rel (na1,None,a1) env) t ar'
+          srec (push_rel (LocalAssum (na1,a1)) env) t ar'
       | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
-	 let env' = push_rel (na1,None,a1) env in
-     let ksort = match (whd_betadeltaiota env' a2) with
+	 let env' = push_rel (LocalAssum (na1,a1)) env in
+     let ksort = match (whd_all env' a2) with
         | Sort s -> family_of_sort s
 	    | _ -> raise (LocalArity None) in
 	  let dep_ind = build_dependent_inductive ind specif params in
@@ -362,8 +318,8 @@ let is_correct_arity env c (p,pj) ind specif params =
       | Sort s', [] ->
 	  check_allowed_sort (family_of_sort s') specif;
 	  false
-      | _, (_,Some _,_ as d)::ar' ->
-	 srec (push_rel d env) (lift 1 pt') ar'
+      | _, (LocalDef _ as d)::ar' ->
+         srec (push_rel d env) (lift 1 pt') ar'
       | _ ->
 	  raise (LocalArity None)
   in
@@ -527,10 +483,10 @@ type guard_env =
 let make_renv env recarg tree =
   { env = env;
     rel_min = recarg+2; (* recarg = 0 ==> Rel 1 -> recarg; Rel 2 -> fix *)
-    genv = [Lazy.lazy_from_val(Subterm(Large,tree))] }
+    genv = [Lazy.from_val(Subterm(Large,tree))] }
 
 let push_var renv (x,ty,spec) =
-  { env = push_rel (x,None,ty) renv.env;
+  { env = push_rel (LocalAssum (x,ty)) renv.env;
     rel_min = renv.rel_min+1;
     genv = spec:: renv.genv }
 
@@ -538,7 +494,7 @@ let assign_var_spec renv (i,spec) =
   { renv with genv = List.assign renv.genv (i-1) spec }
 
 let push_var_renv renv (x,ty) =
-  push_var renv (x,ty,Lazy.lazy_from_val Not_subterm)
+  push_var renv (x,ty,Lazy.from_val Not_subterm)
 
 (* Fetch recursive information about a variable p *)
 let subterm_var p renv =
@@ -549,13 +505,13 @@ let push_ctxt_renv renv ctxt =
   let n = rel_context_length ctxt in
   { env = push_rel_context ctxt renv.env;
     rel_min = renv.rel_min+n;
-    genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
+    genv = iterate (fun ge -> Lazy.from_val Not_subterm::ge) n renv.genv }
 
 let push_fix_renv renv (_,v,_ as recdef) =
   let n = Array.length v in
   { env = push_rec_types recdef renv.env;
     rel_min = renv.rel_min+n;
-    genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
+    genv = iterate (fun ge -> Lazy.from_val Not_subterm::ge) n renv.genv }
 
 
 (* Definition and manipulation of the stack *)
@@ -622,20 +578,21 @@ let check_inductive_codomain env p =
   let env = push_rel_context absctx env in
   let arctx, s = dest_prod_assum env ar in
   let env = push_rel_context arctx env in
-  let i,l' = decompose_app (whd_betadeltaiota env s) in
+  let i,l' = decompose_app (whd_all env s) in
   match i with Ind _ -> true | _ -> false 
 
 (* The following functions are almost duplicated from indtypes.ml, except
 that they carry here a poorer environment (containing less information). *)
 let ienv_push_var (env, lra) (x,a,ra) =
-(push_rel (x,None,a) env, (Norec,ra)::lra)
+(push_rel (LocalAssum (x,a)) env, (Norec,ra)::lra)
 
 let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
   let mib = Environ.lookup_mind mind env in
   let ntypes = mib.mind_ntypes in
   let push_ind specif env =
-     push_rel (Anonymous,None,
-		hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) env
+     let decl = LocalAssum (Anonymous,
+		            hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in
+     push_rel decl env
   in
   let env = Array.fold_right push_ind mib.mind_packets env in
   let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in
@@ -645,7 +602,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
 
 let rec ienv_decompose_prod (env,_ as ienv) n c =
  if Int.equal n 0 then (ienv,c) else
-   let c' = whd_betadeltaiota env c in
+   let c' = whd_all env c in
    match c' with
    Prod(na,a,b) ->
      let ienv' = ienv_push_var ienv (na,a,mk_norec) in
@@ -675,7 +632,7 @@ close to check_positive in indtypes.ml, but does no positivy check and does not
 compute the number of recursive arguments. *)
 let get_recargs_approx env tree ind args =
   let rec build_recargs (env, ra_env as ienv) tree c =
-    let x,largs = decompose_app (whd_betadeltaiota env c) in
+    let x,largs = decompose_app (whd_all env c) in
     match x with
     | Prod (na,b,d) ->
        assert (List.is_empty largs);
@@ -734,7 +691,7 @@ let get_recargs_approx env tree ind args =
 
   and build_recargs_constructors ienv trees c =
     let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c =
-      let x,largs = decompose_app (whd_betadeltaiota env c) in
+      let x,largs = decompose_app (whd_all env c) in
 	match x with
 
           | Prod (na,b,d) ->
@@ -763,7 +720,7 @@ let restrict_spec env spec p =
   let env = push_rel_context absctx env in
   let arctx, s = dest_prod_assum env ar in
   let env = push_rel_context arctx env in
-  let i,args = decompose_app (whd_betadeltaiota env s) in
+  let i,args = decompose_app (whd_all env s) in
   match i with
   | Ind i ->
      begin match spec with
@@ -785,7 +742,7 @@ let restrict_spec env spec p =
 
 let rec subterm_specif renv stack t =
   (* maybe reduction is not always necessary! *)
-  let f,l = decompose_app (whd_betadeltaiota renv.env t) in
+  let f,l = decompose_app (whd_all renv.env t) in
     match f with
       | Rel k -> subterm_var k renv
 
@@ -861,7 +818,7 @@ and stack_element_specif = function
   |SArg x -> x
 
 and extract_stack renv a = function
-  | [] -> Lazy.lazy_from_val Not_subterm , []
+  | [] -> Lazy.from_val Not_subterm , []
   | h::t -> stack_element_specif h, t
 
 
@@ -899,11 +856,11 @@ let filter_stack_domain env ci p stack =
   if noccur_with_meta 1 (rel_context_length absctx) ar then stack
   else let env = push_rel_context absctx env in
   let rec filter_stack env ar stack =
-    let t = whd_betadeltaiota env ar in
+    let t = whd_all env ar in
     match stack, t with
     | elt :: stack', Prod (n,a,c0) ->
-      let d = (n,None,a) in
-      let ty, args = decompose_app (whd_betadeltaiota env a) in
+      let d = LocalAssum (n,a) in
+      let ty, args = decompose_app (whd_all env a) in
       let elt = match ty with
       | Ind ind -> 
         let spec' = stack_element_specif elt in
@@ -956,10 +913,10 @@ let check_one_fix renv recpos trees def =
               end
             else
               begin
-                match pi2 (lookup_rel p renv.env) with
-                | None ->
+                match lookup_rel p renv.env with
+                | LocalAssum _ ->
                     List.iter (check_rec_call renv []) l
-                | Some c ->
+                | LocalDef (_,c,_) ->
                     try List.iter (check_rec_call renv []) l
                     with FixGuardError _ ->
                       check_rec_call renv stack (applist(lift p c,l))
@@ -1032,6 +989,10 @@ let check_one_fix renv recpos trees def =
         | (Ind _ | Construct _) ->
             List.iter (check_rec_call renv []) l
 
+	| Proj (p, c) ->
+            List.iter (check_rec_call renv []) l;
+            check_rec_call renv [] c
+
         | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
 
 	| Sort _ -> assert (l = [])
@@ -1041,8 +1002,6 @@ let check_one_fix renv recpos trees def =
 
         | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
 
-	| Proj (p, c) -> check_rec_call renv [] c
-
   and check_nested_fix_body renv decr recArgsDecrArg body =
     if decr = 0 then
       check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
@@ -1075,10 +1034,10 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     (* check fi does not appear in the k+1 first abstractions,
        gives the type of the k+1-eme abstraction (must be an inductive)  *)
     let rec check_occur env n def =
-      match (whd_betadeltaiota env def) with
+      match (whd_all env def) with
         | Lambda (x,a,b) ->
 	    if noccur_with_meta n nbfix a then
-	      let env' = push_rel (x, None, a) env in
+	      let env' = push_rel (LocalAssum (x,a)) env in
               if n = k+1 then
                 (* get the inductive type of the fixpoint *)
                 let (mind, _) =
@@ -1124,10 +1083,10 @@ let anomaly_ill_typed () =
   anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor")
 
 let rec codomain_is_coind env c =
-  let b = whd_betadeltaiota env c in
+  let b = whd_all env c in
   match b with
     | Prod (x,a,b) ->
-	codomain_is_coind (push_rel (x, None, a) env) b
+	codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
     | _ ->
 	(try find_coinductive env b
         with Not_found ->
@@ -1136,7 +1095,7 @@ let rec codomain_is_coind env c =
 let check_one_cofix env nbfix def deftype =
   let rec check_rec_call env alreadygrd n tree vlra  t =
     if not (noccur_with_meta n nbfix t) then
-      let c,args = decompose_app (whd_betadeltaiota env t) in
+      let c,args = decompose_app (whd_all env t) in
       match c with
 	| Rel p when  n <= p && p < n+nbfix ->
 	    (* recursive call: must be guarded and no nested recursive
@@ -1168,7 +1127,7 @@ let check_one_cofix env nbfix def deftype =
 	| Lambda (x,a,b) ->
 	     assert (args = []);
             if noccur_with_meta n nbfix a then
-              let env' = push_rel (x, None, a) env in
+              let env' = push_rel (LocalAssum (x,a)) env in
               check_rec_call env' alreadygrd (n+1) tree vlra b
             else
 	      raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 3ea5ed0d..7f93e156 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -18,7 +18,7 @@ let refresh_arity ar =
   let ctxt, hd = decompose_prod_assum ar in
   match hd with
       Sort (Type u) when not (Univ.is_univ_variable u) ->
-      let ul = Univ.Level.make empty_dirpath 1 in
+      let ul = Univ.Level.make DirPath.empty 1 in
       let u' = Univ.Universe.make ul in
       let cst = Univ.enforce_leq u u' Univ.empty_constraint in
       let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in
@@ -26,7 +26,7 @@ let refresh_arity ar =
     | _ -> ar, Univ.ContextSet.empty
 
 let check_constant_declaration env kn cb =
-  Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn); pp_flush ();
+  Flags.if_verbose Feedback.msg_notice (str "  checking cst: " ++ prcon kn);
   let env' =
     if cb.const_polymorphic then
       let inst = Univ.make_abstract_instance cb.const_universes in
@@ -70,7 +70,7 @@ let check_constant_declaration env kn cb =
 let lookup_module mp env =
   try Environ.lookup_module mp env
   with Not_found ->
-    failwith ("Unknown module: "^string_of_mp mp)
+    failwith ("Unknown module: "^ModPath.to_string mp)
 
 let mk_mtb mp sign delta =
   { mod_mp = mp;
diff --git a/checker/modops.ml b/checker/modops.ml
index 9f437526..b720fb62 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (*i*)
-open Errors
+open CErrors
 open Util
 open Pp
 open Names
@@ -28,7 +28,7 @@ let error_not_match l _ =
 let error_no_such_label l = error ("No such label "^Label.to_string l)
 
 let error_no_such_label_sub l l1 =
-  let l1 = string_of_mp l1 in
+  let l1 = ModPath.to_string l1 in
   error ("The field "^
          Label.to_string l^" is missing in "^l1^".")
 
diff --git a/checker/print.ml b/checker/print.ml
index 9cd8fda5..7ef752b0 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -10,7 +10,9 @@ open Format
 open Cic
 open Names
 
-let print_instance i = Pp.pp (Univ.Instance.pr i)
+let chk_pp = Pp.pp_with Format.std_formatter
+
+let print_instance i = chk_pp (Univ.Instance.pr i)
 
 let print_pure_constr csr =
   let rec term_display c = match  c with
@@ -108,7 +110,7 @@ let print_pure_constr csr =
   and sort_display = function
     | Prop(Pos) -> print_string "Set"
     | Prop(Null) -> print_string "Prop"
-    | Type u -> print_string "Type("; Pp.pp (Univ.pr_uni u); print_string ")"
+    | Type u -> print_string "Type("; chk_pp (Univ.pr_uni u); print_string ")"
 
   and name_display = function
     | Name id -> print_string (Id.to_string id)
@@ -122,7 +124,7 @@ let print_pure_constr csr =
 	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (debug_string_of_mind sp)
+      print_string (MutInd.debug_to_string sp)
   and sp_con_display sp =
 (*    let dir,l = decode_kn sp in
     let ls =
@@ -131,7 +133,7 @@ let print_pure_constr csr =
 	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (debug_string_of_con sp)
+      print_string (Constant.debug_to_string sp)
 
   in
     try
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 3a666a60..ec16aa26 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Cic
 open Term
@@ -92,13 +92,13 @@ let whd_betaiotazeta x =
        Prod _|Lambda _|Fix _|CoFix _) -> x
     | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x)
 
-let whd_betadeltaiota env t =
+let whd_all env t =
   match t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> t
     | _ -> whd_val (create_clos_infos betadeltaiota env) (inject t)
 
-let whd_betadeltaiota_nolet env t =
+let whd_allnolet env t =
   match t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t
@@ -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)
@@ -476,7 +477,7 @@ let vm_conv cv_pb = fconv cv_pb true
  * error message. *)
 
 let hnf_prod_app env t n =
-  match whd_betadeltaiota env t with
+  match whd_all env t with
     | Prod (_,_,b) -> subst1 n b
     | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
 
@@ -487,10 +488,10 @@ let hnf_prod_applist env t nl =
 
 let dest_prod env =
   let rec decrec env m c =
-    let t = whd_betadeltaiota env c in
+    let t = whd_all env c in
     match t with
       | Prod (n,a,c0) ->
-          let d = (n,None,a) in
+          let d = LocalAssum (n,a) in
 	  decrec (push_rel d env) (d::m) c0
       | _ -> m,t
   in
@@ -499,17 +500,17 @@ let dest_prod env =
 (* The same but preserving lets in the context, not internal ones. *)
 let dest_prod_assum env =
   let rec prodec_rec env l ty =
-    let rty = whd_betadeltaiota_nolet env ty in
+    let rty = whd_allnolet env ty in
     match rty with
     | Prod (x,t,c)  ->
-        let d = (x,None,t) in
+        let d = LocalAssum (x,t) in
 	prodec_rec (push_rel d env) (d::l) c
     | LetIn (x,b,t,c) ->
-        let d = (x,Some b,t) in
+        let d = LocalDef (x,b,t) in
 	prodec_rec (push_rel d env) (d::l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               ->
-      let rty' = whd_betadeltaiota env rty in
+      let rty' = whd_all env rty in
 	if Term.eq_constr rty' rty then l, rty
 	else prodec_rec env l rty'
   in
@@ -517,13 +518,13 @@ let dest_prod_assum env =
 
 let dest_lam_assum env =
   let rec lamec_rec env l ty =
-    let rty = whd_betadeltaiota_nolet env ty in
+    let rty = whd_allnolet env ty in
     match rty with
     | Lambda (x,t,c)  ->
-        let d = (x,None,t) in
+        let d = LocalAssum (x,t) in
 	lamec_rec (push_rel d env) (d::l) c
     | LetIn (x,b,t,c) ->
-        let d = (x,Some b,t) in
+        let d = LocalDef (x,b,t) in
 	lamec_rec (push_rel d env) (d::l) c
     | Cast (c,_,_)    -> lamec_rec env l c
     | _               -> l,rty
diff --git a/checker/reduction.mli b/checker/reduction.mli
index 2f551f4a..15a2df1f 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -16,8 +16,8 @@ open Environ
 (*s Reduction functions *)
 
 val whd_betaiotazeta        : constr -> constr
-val whd_betadeltaiota       : env -> constr -> constr
-val whd_betadeltaiota_nolet : env -> constr -> constr
+val whd_all       : env -> constr -> constr
+val whd_allnolet : env -> constr -> constr
 
 (************************************************************************)
 (*s conversion functions *)
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index fa429755..11cd742b 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -7,12 +7,14 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Cic
 open Names
 open Environ
 
+let pr_dirpath dp = str (DirPath.to_string dp)
+
 (************************************************************************)
 (*
  * Global environment
@@ -33,28 +35,23 @@ 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."
+        CErrors.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 *)
 
 let report_clash f caller dir =
   let msg =
-    str "compiled library " ++ str(DirPath.to_string caller) ++
+    str "compiled library " ++ pr_dirpath caller ++
     spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++
-    str(DirPath.to_string dir) ++ fnl() in
+    pr_dirpath dir ++ fnl() in
   f msg
 
 
@@ -79,7 +76,7 @@ let stamp_library file digest = ()
    warning is issued in case of mismatch *)
 let import file clib univs digest =
   let env = !genv in
-  check_imports msg_warning clib.comp_name env clib.comp_deps;
+  check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;
   let mb = clib.comp_mod in
   Mod_checking.check_module
@@ -91,7 +88,7 @@ let import file clib univs digest =
 (* When the module is admitted, digests *must* match *)
 let unsafe_import file clib univs digest =
   let env = !genv in
-  if !Flags.debug then check_imports msg_warning clib.comp_name env clib.comp_deps
+  if !Flags.debug then check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps
   else check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;
   full_add_module clib.comp_name clib.comp_mod univs digest
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index e4192257..7eae9b83 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (*i*)
-open Errors
+open CErrors
 open Util
 open Names
 open Cic
@@ -103,7 +103,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   in
   let eq_projection_body p1 p2 =
     let check eq f = if not (eq (f p1) (f p2)) then error () in
-    check eq_mind (fun x -> x.proj_ind);
+    check MutInd.equal (fun x -> x.proj_ind);
     check (==) (fun x -> x.proj_npars);
     check (==) (fun x -> x.proj_arg);
     check (eq_constr) (fun x -> x.proj_type);
@@ -302,7 +302,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
 		let c2 = force_constr lc2 in
 		check_conv conv env c1 c2))
       | IndType ((kn,i),mind1) ->
-	  ignore (Errors.error (
+	  ignore (CErrors.error (
 		    "The kernel does not recognize yet that a parameter can be " ^
 		      "instantiated by an inductive type. Hint: you can rename the " ^
 		      "inductive type and give a definition to map the old name to the new " ^
@@ -313,7 +313,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
-      ignore (Errors.error (
+      ignore (CErrors.error (
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by a constructor. Hint: you can rename the " ^
        "constructor and give a definition to map the old name to the new " ^
diff --git a/checker/term.ml b/checker/term.ml
index 6487d1a1..591348cb 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -8,7 +8,7 @@
 
 (* This module instantiates the structure of generic deBruijn terms to Coq *)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Esubst
@@ -222,24 +222,29 @@ let rel_context_length = List.length
 let rel_context_nhyps hyps =
   let rec nhyps acc = function
     | [] -> acc
-    | (_,None,_)::hyps -> nhyps (1+acc) hyps
-    | (_,Some _,_)::hyps -> nhyps acc hyps in
+    | LocalAssum _ :: hyps -> nhyps (1+acc) hyps
+    | LocalDef _ :: hyps -> nhyps acc hyps in
   nhyps 0 hyps
 let fold_rel_context f l ~init = List.fold_right f l init
 
-let map_rel_context f l =
-  let map_decl (n, body_o, typ as decl) =
-    let body_o' = Option.smartmap f body_o in
-    let typ' = f typ in
-      if body_o' == body_o && typ' == typ then decl else
-	(n, body_o', typ')
-  in
-    List.smartmap map_decl l
+let map_rel_decl f = function
+  | LocalAssum (n, typ) as decl ->
+     let typ' = f typ in
+     if typ' == typ then decl else
+       LocalAssum (n, typ')
+  | LocalDef (n, body, typ) as decl ->
+     let body' = f body in
+     let typ' = f typ in
+     if body' == body && typ' == typ then decl else
+       LocalDef (n, body', typ')
+
+let map_rel_context f =
+  List.smartmap (map_rel_decl f)
 
 let extended_rel_list n hyps =
   let rec reln l p = function
-    | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
-    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
+    | LocalDef _ :: hyps -> reln l (p+1) hyps
     | [] -> l
   in
   reln [] 1 hyps
@@ -272,8 +277,8 @@ let decompose_lam_n_assum n =
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else match c with
-    | Lambda (x,t,c)  -> lamdec_rec ((x,None,t) :: l) (n-1) c
-    | LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c
+    | Lambda (x,t,c)  -> lamdec_rec (LocalAssum (x,t) :: l) (n-1) c
+    | LetIn (x,b,t,c) -> lamdec_rec (LocalDef (x,b,t) :: l) n c
     | Cast (c,_,_)      -> lamdec_rec l n c
     | c -> error "decompose_lam_n_assum: not enough abstractions"
   in
@@ -282,18 +287,18 @@ let decompose_lam_n_assum n =
 (* Iterate products, with or without lets *)
 
 (* Constructs either [(x:t)c] or [[x=b:t]c] *)
-let mkProd_or_LetIn (na,body,t) c =
-  match body with
-    | None -> Prod (na, t, c)
-    | Some b -> LetIn (na, b, t, c)
+let mkProd_or_LetIn decl c =
+  match decl with
+    | LocalAssum (na,t) -> Prod (na, t, c)
+    | LocalDef (na,b,t) -> LetIn (na, b, t, c)
 
 let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
 
 let decompose_prod_assum =
   let rec prodec_rec l c =
     match c with
-    | Prod (x,t,c)    -> prodec_rec ((x,None,t) :: l) c
-    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) c
+    | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t) :: l) c
+    | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c
     | Cast (c,_,_)    -> prodec_rec l c
     | _               -> l,c
   in
@@ -305,8 +310,8 @@ let decompose_prod_n_assum n =
   let rec prodec_rec l n c =
     if Int.equal n 0 then l,c
     else match c with
-    | Prod (x,t,c)    -> prodec_rec ((x,None,t) :: l) (n-1) c
-    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c
+    | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t) :: l) (n-1) c
+    | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) (n-1) c
     | Cast (c,_,_)    -> prodec_rec l n c
     | c -> error "decompose_prod_n_assum: not enough assumptions"
   in
@@ -324,8 +329,8 @@ let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign
 let destArity =
   let rec prodec_rec l c =
     match c with
-    | Prod (x,t,c)    -> prodec_rec ((x,None,t)::l) c
-    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
+    | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t)::l) c
+    | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t)::l) c
     | Cast (c,_,_)    -> prodec_rec l c
     | Sort s          -> l,s
     | _               -> anomaly ~label:"destArity" (Pp.str "not an arity")
diff --git a/checker/term.mli b/checker/term.mli
index ab488b2b..0af83e05 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -35,12 +35,13 @@ val rel_context_length : rel_context -> int
 val rel_context_nhyps : rel_context -> int
 val fold_rel_context :
   (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration
 val map_rel_context : (constr -> constr) -> rel_context -> rel_context
 val extended_rel_list : int -> rel_context -> constr list
 val compose_lam : (name * constr) list -> constr -> constr
 val decompose_lam : constr -> (name * constr) list * constr
 val decompose_lam_n_assum : int -> constr -> rel_context * constr
-val mkProd_or_LetIn : name * constr option * constr -> constr -> constr
+val mkProd_or_LetIn : rel_declaration -> constr -> constr
 val it_mkProd_or_LetIn : constr -> rel_context -> constr
 val decompose_prod_assum : constr -> rel_context * constr
 val decompose_prod_n_assum : int -> constr -> rel_context * constr
diff --git a/checker/typeops.ml b/checker/typeops.ml
index d49c40a8..173e19ce 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Cic
@@ -33,7 +33,7 @@ let check_constraints cst env =
 
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env (c,ty as j) =
-  match whd_betadeltaiota env ty with
+  match whd_all env ty with
     | Sort s -> (c,s)
     | _ -> error_not_type env j
 
@@ -62,7 +62,7 @@ let judge_of_type u = Sort (Type (Univ.super u))
 
 let judge_of_relative env n =
   try
-    let (_,_,typ) = lookup_rel n env in
+    let LocalAssum (_,typ) | LocalDef (_,_,typ) = lookup_rel n env in
     lift n typ
   with Not_found ->
     error_unbound_rel env n
@@ -92,7 +92,7 @@ let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp =
   let _cb =
     try lookup_constant kn env
     with Not_found ->
-      failwith ("Cannot find constant: "^string_of_con kn)
+      failwith ("Cannot find constant: "^Constant.to_string kn)
   in
   let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in
   let () = check_constraints cu env in
@@ -107,7 +107,7 @@ let judge_of_apply env (f,funj) argjv =
   let rec apply_rec n typ = function
     | [] -> typ
     | (h,hj)::restjl ->
-        (match whd_betadeltaiota env typ with
+        (match whd_all env typ with
           | Prod (_,c1,c2) ->
 	      (try conv_leq env hj c1
 	      with NotConvertible ->
@@ -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
@@ -178,7 +178,7 @@ let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) =
   let specif =
     try lookup_mind_specif env ind
     with Not_found ->
-      failwith ("Cannot find inductive: "^string_of_mind (fst ind))
+      failwith ("Cannot find inductive: "^MutInd.to_string (fst ind))
   in
   type_of_inductive_knowing_parameters env (specif,u) paramstyp
 
@@ -192,7 +192,7 @@ let judge_of_constructor env (c,u) =
   let specif =
     try lookup_mind_specif env ind
     with Not_found ->
-      failwith ("Cannot find inductive: "^string_of_mind (fst ind))
+      failwith ("Cannot find inductive: "^MutInd.to_string (fst ind))
   in
   type_of_constructor (c,u) specif
 
@@ -223,7 +223,7 @@ let judge_of_projection env p c ct =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (c, ct)
   in
-    assert(eq_mind pb.proj_ind (fst ind));
+    assert(MutInd.equal pb.proj_ind (fst ind));
     let ty = subst_instance_constr u pb.proj_type in
       substl (c :: List.rev args) ty
 
@@ -296,13 +296,13 @@ let rec execute env cstr =
 
     | Lambda (name,c1,c2) ->
         let _ = execute_type env c1 in
-	let env1 = push_rel (name,None,c1) env in
+	let env1 = push_rel (LocalAssum (name,c1)) env in
         let j' = execute env1 c2 in
         Prod(name,c1,j')
 
     | Prod (name,c1,c2) ->
         let varj = execute_type env c1 in
-	let env1 = push_rel (name,None,c1) env in
+	let env1 = push_rel (LocalAssum (name,c1)) env in
         let varj' = execute_type env1 c2 in
 	Sort (sort_of_product env varj varj')
 
@@ -314,7 +314,7 @@ let rec execute env cstr =
           let env',c2' = (* refresh_arity env *) env, c2 in
           let _ = execute_type env' c2' in
           judge_of_cast env' (c1,j1) DEFAULTcast c2' in
-        let env1 = push_rel (name,Some c1,c2) env in
+        let env1 = push_rel (LocalDef (name,c1,c2)) env in
         let j' = execute env1 c3 in
         subst1 c1 j'
 
@@ -378,10 +378,10 @@ let infer_type env constr = execute_type env constr
 let check_ctxt env rels =
   fold_rel_context (fun d env ->
     match d with
-        (_,None,ty) ->
+      | LocalAssum (_,ty) ->
           let _ = infer_type env ty in
           push_rel d env
-      | (_,Some bd,ty) ->
+      | LocalDef (_,bd,ty) ->
           let j1 = infer env bd in
           let _ = infer env ty in
           conv_leq env j1 ty;
@@ -399,9 +399,9 @@ let check_polymorphic_arity env params par =
   let pl = par.template_param_levels in
   let rec check_p env pl params =
     match pl, params with
-        Some u::pl, (na,None,ty)::params ->
+        Some u::pl, LocalAssum (na,ty)::params ->
           check_kind env ty u;
-          check_p (push_rel (na,None,ty) env) pl params
+          check_p (push_rel (LocalAssum (na,ty)) env) pl params
       | None::pl,d::params -> check_p (push_rel d env) pl params
       | [], _ -> ()
       | _ -> failwith "check_poly: not the right number of params" in
diff --git a/checker/univ.ml b/checker/univ.ml
index cb2eaced..668f3a05 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -14,7 +14,7 @@
 (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 
 (* Universes are stratified by a partial ordering $\le$.
@@ -33,7 +33,7 @@ module type Hashconsed =
 sig
   type t
   val hash : t -> int
-  val equal : t -> t -> bool
+  val eq : t -> t -> bool
   val hcons : t -> t
 end
 
@@ -51,7 +51,7 @@ struct
     type t = _t
     type u = (M.t -> M.t)
     let hash = function Nil -> 0 | Cons (_, h, _) -> h
-    let equal l1 l2 = match l1, l2 with
+    let eq l1 l2 = match l1, l2 with
     | Nil, Nil -> true
     | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2
     | _ -> false
@@ -131,7 +131,7 @@ module HList = struct
   let rec remove x = function
   | Nil -> nil
   | Cons (y, _, l) ->
-    if H.equal x y then l
+    if H.eq x y then l
     else cons y (remove x l)
 
   end
@@ -229,7 +229,7 @@ module Level = struct
     type _t = t
     type t = _t
     type u = unit
-    let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data
+    let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data
     let hash x = x.hash
     let hashcons () x =
       let data' = RawLevel.hcons x.data in
@@ -320,7 +320,7 @@ struct
       let hashcons hdir (b,n as x) = 
 	let b' = hdir b in 
 	  if b' == b then x else (b',n)
-      let equal l1 l2 =
+      let eq l1 l2 =
         l1 == l2 || 
         match l1,l2 with
 	| (b,n), (b',n') -> b == b' && n == n'
@@ -339,7 +339,7 @@ struct
       let hcons =
         Hashcons.simple_hcons H.generate H.hcons Level.hcons
       let hash = ExprHash.hash
-      let equal x y = x == y ||
+      let eq x y = x == y ||
         (let (u,n) = x and (v,n') = y in
            Int.equal n n' && Level.equal u v)
 
@@ -1089,7 +1089,7 @@ struct
 	  a
 	end
 
-    let equal t1 t2 =
+    let eq t1 t2 =
       t1 == t2 ||
 	(Int.equal (Array.length t1) (Array.length t2) &&
 	   let rec aux i =
diff --git a/checker/values.ml b/checker/values.ml
index c14e9223..c175aed6 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 7c050ff1db22f14ee3a4c44aae533082 checker/cic.mli
+MD5 6466d8cc443b5896cb905776df0cc49e  checker/cic.mli
 
 *)
 
@@ -154,8 +154,8 @@ and v_prec = Tuple ("prec_declaration",
 and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|])
 and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|])
 
-
-let v_rdecl = v_tuple "rel_declaration" [|v_name;Opt v_constr;v_constr|]
+let v_rdecl = v_sum "rel_declaration" 0 [| [|v_name; v_constr|];               (* LocalAssum *)
+                                           [|v_name; v_constr; v_constr|] |]   (* LocalDef *)
 let v_rctxt = List v_rdecl
 
 let v_section_ctxt = v_enum "emptylist" 1
@@ -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|]
@@ -213,6 +212,9 @@ let v_projbody =
 	    v_tuple "proj_eta" [|v_constr;v_constr|];
 	    v_constr|]
 
+let v_typing_flags =
+  v_tuple "typing_flags" [|v_bool; v_bool|]
+
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
     v_cst_def;
@@ -221,7 +223,8 @@ let v_cb = v_tuple "constant_body"
     v_bool;
     v_context;
     Opt v_projbody;
-    v_bool|]
+    v_bool;
+    v_typing_flags|]
 
 let v_recarg = v_sum "recarg" 1 (* Norec *)
   [|[|v_ind|] (* Mrec *);[|v_ind|] (* Imbr *)|]
@@ -270,7 +273,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     v_rctxt;
     v_bool;
     v_context;
-    Opt v_bool|]
+    Opt v_bool;
+    v_typing_flags|]
 
 let v_with =
   Sum ("with_declaration_body",0,
diff --git a/checker/votour.ml b/checker/votour.ml
index 78978bb2..48f9f45e 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -10,6 +10,26 @@ open Values
 
 (** {6 Interactive visit of a vo} *)
 
+let rec read_num max =
+  let quit () =
+    Printf.printf "\nGoodbye!\n%!";
+    exit 0 in
+  Printf.printf "# %!";
+  let l = try read_line () with End_of_file -> quit () in
+  if l = "u" then None
+  else if l = "x" then quit ()
+  else
+    try
+      let v = int_of_string l in
+      if v < 0 || v >= max then
+        let () =
+          Printf.printf "Out-of-range input! (only %d children)\n%!" max in
+        read_num max
+      else Some v
+    with Failure "int_of_string" ->
+      Printf.printf "Unrecognized input! <n> enters the <n>-th child, u goes up 1 level, x exits\n%!";
+      read_num max
+
 type 'a repr =
 | INT of int
 | STRING of string
@@ -22,6 +42,7 @@ sig
   val input : in_channel -> obj
   val repr : obj -> obj repr
   val size : obj -> int
+  val oid : obj -> int option
 end
 
 module ReprObj : S =
@@ -45,6 +66,7 @@ struct
     else INT (Obj.magic obj)
 
   let size (_, p) = CObj.shared_size_of_pos p
+  let oid _ = None
 end
 
 module ReprMem : S =
@@ -97,6 +119,9 @@ struct
     let _ = init_size seen obj in
     obj
 
+  let oid = function
+  | Int _ | Atm _ | Fun _ -> None
+  | Ptr p -> Some p
 end
 
 module Visit (Repr : S) :
@@ -149,9 +174,13 @@ let rec get_details v o = match v, Repr.repr o with
   |Annot (s,v), _ -> get_details v o
   |_ -> ""
 
+let get_oid obj = match Repr.oid obj with
+| None -> ""
+| Some id -> Printf.sprintf " [0x%08x]" id
+
 let node_info (v,o,p) =
   get_name ~extra:true v ^ get_details v o ^
-    " (size "^ string_of_int (Repr.size o)^"w)"
+    " (size "^ string_of_int (Repr.size o)^"w)" ^ get_oid o
 
 (** Children of a block : type, object, position.
     For lists, we collect all elements of the list at once *)
@@ -246,15 +275,13 @@ let rec visit v o pos =
     (fun i vop -> Printf.printf "  %d: %s\n" i (node_info vop))
     children;
   Printf.printf "-------------\n";
-  Printf.printf ("# %!");
-  let l = read_line () in
   try
-    if l = "u" then let info = pop () in visit info.typ info.obj info.pos
-    else if l = "x" then (Printf.printf "\nGoodbye!\n\n";exit 0)
-    else
-      let v',o',pos' = children.(int_of_string l) in
-      push (get_name v) v o pos;
-      visit v' o' pos'
+    match read_num (Array.length children) with
+    | None -> let info = pop () in visit info.typ info.obj info.pos
+    | Some child ->
+       let v',o',pos' = children.(child) in
+       push (get_name v) v o pos;
+       visit v' o' pos'
   with
   | Failure "empty stack" -> ()
   | Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos
@@ -341,13 +368,13 @@ let visit_vo f =
       let size = if Sys.word_size = 64 then header.size64 else header.size32 in
       Printf.printf "  %d: %s, starting at byte %d (size %iw)\n" i name pos size)
       segments;
-    Printf.printf "# %!";
-    let l = read_line () in
-    let seg = int_of_string l in
-    seek_in ch segments.(seg).pos;
-    let o = Repr.input ch in
-    let () = Visit.init () in
-    Visit.visit segments.(seg).typ o []
+    match read_num (Array.length segments) with
+    | Some seg ->
+       seek_in ch segments.(seg).pos;
+       let o = Repr.input ch in
+       let () = Visit.init () in
+       Visit.visit segments.(seg).typ o []
+    | None -> ()
   done
 
 let main =