Imported Upstream version 8.5~beta3+dfsg

27 files changed, 835 insertions, 236 deletions

diff --git a/checker/analyze.ml b/checker/analyze.ml
new file mode 100644
index 00000000..c48b8301
--- /dev/null
+++ b/checker/analyze.ml
@@ -0,0 +1,350 @@
+(** Headers *)
+
+let prefix_small_block =         0x80
+let prefix_small_int =           0x40
+let prefix_small_string =        0x20
+
+let code_int8 =                  0x00
+let code_int16 =                 0x01
+let code_int32 =                 0x02
+let code_int64 =                 0x03
+let code_shared8 =               0x04
+let code_shared16 =              0x05
+let code_shared32 =              0x06
+let code_double_array32_little = 0x07
+let code_block32 =               0x08
+let code_string8 =               0x09
+let code_string32 =              0x0A
+let code_double_big =            0x0B
+let code_double_little =         0x0C
+let code_double_array8_big =     0x0D
+let code_double_array8_little =  0x0E
+let code_double_array32_big =    0x0F
+let code_codepointer =           0x10
+let code_infixpointer =          0x11
+let code_custom =                0x12
+let code_block64 =               0x13
+
+type code_descr =
+| CODE_INT8
+| CODE_INT16
+| CODE_INT32
+| CODE_INT64
+| CODE_SHARED8
+| CODE_SHARED16
+| CODE_SHARED32
+| CODE_DOUBLE_ARRAY32_LITTLE
+| CODE_BLOCK32
+| CODE_STRING8
+| CODE_STRING32
+| CODE_DOUBLE_BIG
+| CODE_DOUBLE_LITTLE
+| CODE_DOUBLE_ARRAY8_BIG
+| CODE_DOUBLE_ARRAY8_LITTLE
+| CODE_DOUBLE_ARRAY32_BIG
+| CODE_CODEPOINTER
+| CODE_INFIXPOINTER
+| CODE_CUSTOM
+| CODE_BLOCK64
+
+let code_max = 0x13
+
+let magic_number = "\132\149\166\190"
+
+(** Memory reification *)
+
+type repr =
+| RInt of int
+| RBlock of (int * int) (* tag × len *)
+| RString of string
+| RPointer of int
+| RCode of int
+
+type data =
+| Int of int (* value *)
+| Ptr of int (* pointer *)
+| Atm of int (* tag *)
+| Fun of int (* address *)
+
+type obj =
+| Struct of int * data array (* tag × data *)
+| String of string
+
+module type Input =
+sig
+  type t
+  val input_byte : t -> int
+  val input_binary_int : t -> int
+end
+
+module type S =
+sig
+  type input
+  val parse : input -> (data * obj array)
+end
+
+module Make(M : Input) =
+struct
+
+open M
+
+type input = M.t
+
+let current_offset = ref 0
+
+let input_byte chan =
+  let () = incr current_offset in
+  input_byte chan
+
+let input_binary_int chan =
+  let () = current_offset := !current_offset + 4 in
+  input_binary_int chan
+
+let input_char chan = Char.chr (input_byte chan)
+
+let parse_header chan =
+  let () = current_offset := 0 in
+  let magic = String.create 4 in
+  let () = for i = 0 to 3 do magic.[i] <- input_char chan done in
+  let length = input_binary_int chan in
+  let objects = input_binary_int chan in
+  let size32 = input_binary_int chan in
+  let size64 = input_binary_int chan in
+  (magic, length, size32, size64, objects)
+
+let input_int8s chan =
+  let i = input_byte chan in
+  if i land 0x80 = 0
+    then i
+    else i lor ((-1) lsl 8)
+
+let input_int8u = input_byte
+
+let input_int16s chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let ans = (i lsl 8) lor j in
+  if i land 0x80 = 0
+    then ans
+    else ans lor ((-1) lsl 16)
+
+let input_int16u chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  (i lsl 8) lor j
+
+let input_int32s chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in
+  if i land 0x80 = 0
+    then ans
+    else ans lor ((-1) lsl 31)
+
+let input_int32u chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l
+
+let input_int64s chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  let m = input_byte chan in
+  let n = input_byte chan in
+  let o = input_byte chan in
+  let p = input_byte chan in
+  let ans =
+    (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor
+    (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p
+  in
+  if i land 0x80 = 0
+    then ans
+    else ans lor ((-1) lsl 63)
+
+let input_int64u chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  let m = input_byte chan in
+  let n = input_byte chan in
+  let o = input_byte chan in
+  let p = input_byte chan in
+  (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor
+  (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p
+
+let input_header32 chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  let tag = l in
+  let len = (i lsl 14) lor (j lsl 6) lor (k lsr 2) in
+  (tag, len)
+
+let input_header64 chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  let m = input_byte chan in
+  let n = input_byte chan in
+  let o = input_byte chan in
+  let p = input_byte chan in
+  let tag = p in
+  let len =
+    (i lsl 46) lor (j lsl 38) lor (k lsl 30) lor (l lsl 22) lor
+    (m lsl 14) lor (n lsl 6) lor (o lsr 2)
+  in
+  (tag, len)
+
+let input_string len chan =
+  let ans = String.create len in
+  for i = 0 to pred len do
+    ans.[i] <- input_char chan;
+  done;
+  ans
+
+let parse_object chan =
+  let data = input_byte chan in
+  if prefix_small_block <= data then
+    let tag = data land 0x0F in
+    let len = (data lsr 4) land 0x07 in
+    RBlock (tag, len)
+  else if prefix_small_int <= data then
+    RInt (data land 0x3F)
+  else if prefix_small_string <= data then
+    let len = data land 0x1F in
+    RString (input_string len chan)
+  else if data > code_max then
+    assert false
+  else match (Obj.magic data) with
+  | CODE_INT8 ->
+    RInt (input_int8s chan)
+  | CODE_INT16 ->
+    RInt (input_int16s chan)
+  | CODE_INT32 ->
+    RInt (input_int32s chan)
+  | CODE_INT64 ->
+    RInt (input_int64s chan)
+  | CODE_SHARED8 ->
+    RPointer (input_int8u chan)
+  | CODE_SHARED16 ->
+    RPointer (input_int16u chan)
+  | CODE_SHARED32 ->
+    RPointer (input_int32u chan)
+  | CODE_BLOCK32 ->
+    RBlock (input_header32 chan)
+  | CODE_BLOCK64 ->
+    RBlock (input_header64 chan)
+  | CODE_STRING8 ->
+    let len = input_int8u chan in
+    RString (input_string len chan)
+  | CODE_STRING32 ->
+    let len = input_int32u chan in
+    RString (input_string len chan)
+  | CODE_CODEPOINTER ->
+    let addr = input_int32u chan in
+    for i = 0 to 15 do ignore (input_byte chan); done;
+    RCode addr
+  | CODE_DOUBLE_ARRAY32_LITTLE
+  | CODE_DOUBLE_BIG
+  | CODE_DOUBLE_LITTLE
+  | CODE_DOUBLE_ARRAY8_BIG
+  | CODE_DOUBLE_ARRAY8_LITTLE
+  | CODE_DOUBLE_ARRAY32_BIG
+  | CODE_INFIXPOINTER
+  | CODE_CUSTOM ->
+    Printf.eprintf "Unhandled code %04x\n%!" data; assert false
+
+let parse chan =
+  let (magic, len, _, _, size) = parse_header chan in
+  let () = assert (magic = magic_number) in
+  let memory = Array.make size (Struct ((-1), [||])) in
+  let current_object = ref 0 in
+  let fill_obj = function
+  | RPointer n ->
+    let data = Ptr (!current_object - n) in
+    data, None
+  | RInt n ->
+    let data = Int n in
+    data, None
+  | RString s ->
+    let data = Ptr !current_object in
+    let () = memory.(!current_object) <- String s in
+    let () = incr current_object in
+    data, None
+  | RBlock (tag, 0) ->
+    (* Atoms are never shared *)
+    let data = Atm tag in
+    data, None
+  | RBlock (tag, len) ->
+    let data = Ptr !current_object in
+    let nblock = Array.make len (Atm (-1)) in
+    let () = memory.(!current_object) <- Struct (tag, nblock) in
+    let () = incr current_object in
+    data, Some nblock
+  | RCode addr ->
+    let data = Fun addr in
+    data, None
+  in
+
+  let rec fill block off accu =
+    if Array.length block = off then
+      match accu with
+      | [] -> ()
+      | (block, off) :: accu -> fill block off accu
+    else
+      let data, nobj = fill_obj (parse_object chan) in
+      let () = block.(off) <- data in
+      let block, off, accu = match nobj with
+      | None -> block, succ off, accu
+      | Some nblock -> nblock, 0, ((block, succ off) :: accu)
+      in
+      fill block off accu
+  in
+  let ans = [|Atm (-1)|] in
+  let () = fill ans 0 [] in
+  (ans.(0), memory)
+
+end
+
+module IChannel =
+struct
+  type t = in_channel
+  let input_byte = Pervasives.input_byte
+  let input_binary_int = Pervasives.input_binary_int
+end
+
+module IString =
+struct
+  type t = (string * int ref)
+
+  let input_byte (s, off) =
+    let ans = Char.code (s.[!off]) in
+    let () = incr off in
+    ans
+
+  let input_binary_int chan =
+    let i = input_byte chan in
+    let j = input_byte chan in
+    let k = input_byte chan in
+    let l = input_byte chan in
+    let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in
+    if i land 0x80 = 0
+      then ans
+      else ans lor ((-1) lsl 31)
+
+end
+
+module PChannel = Make(IChannel)
+module PString = Make(IString)
+
+let parse_channel = PChannel.parse
+let parse_string s = PString.parse (s, ref 0)
diff --git a/checker/analyze.mli b/checker/analyze.mli
new file mode 100644
index 00000000..42efcf01
--- /dev/null
+++ b/checker/analyze.mli
@@ -0,0 +1,35 @@
+type data =
+| Int of int
+| Ptr of int
+| Atm of int (* tag *)
+| Fun of int (* address *)
+
+type obj =
+| Struct of int * data array (* tag × data *)
+| String of string
+
+val parse_channel : in_channel -> (data * obj array)
+val parse_string : string -> (data * obj array)
+
+(** {6 Functorized version} *)
+
+module type Input =
+sig
+  type t
+  val input_byte : t -> int
+  (** Input a single byte *)
+  val input_binary_int : t -> int
+  (** Input a big-endian 31-bits signed integer *)
+end
+(** Type of inputs *)
+
+module type S =
+sig
+  type input
+  val parse : input -> (data * obj array)
+  (** Return the entry point and the reification of the memory out of a
+      marshalled structure. *)
+end
+
+module Make (M : Input) : S with type input = M.t
+(** Functorized version of the previous code. *)
diff --git a/checker/check.ml b/checker/check.ml
index 3e22c4b1..21c8f1c5 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -46,7 +46,7 @@ type library_t = {
   library_opaques : Cic.opaque_table;
   library_deps : Cic.library_deps;
   library_digest : Cic.vodigest;
-  library_extra_univs : Univ.constraints }
+  library_extra_univs : Univ.ContextSet.t }
 
 module LibraryOrdered =
   struct
@@ -97,7 +97,7 @@ let access_opaque_univ_table dp i =
     let t = LibraryMap.find dp !opaque_univ_tables in
     assert (i < Array.length t);
     Future.force t.(i)
-  with Not_found -> Univ.empty_constraint
+  with Not_found -> Univ.ContextSet.empty
 
 
 let _ = Declarations.indirect_opaque_access := access_opaque_table
@@ -271,32 +271,22 @@ let try_locate_qualified_library qid =
     | LibNotFound -> error_lib_not_found qid
 
 (************************************************************************)
-(*s Low-level interning/externing of libraries to files *)
+(*s Low-level interning of libraries from files *)
 
-(*s Loading from disk to cache (preparation phase) *)
-
-let raw_intern_library =
-  snd (System.raw_extern_intern Coq_config.vo_magic_number)
-
-let with_magic_number_check f a =
-  try f a
-  with System.Bad_magic_number fname ->
-    errorlabstrm "with_magic_number_check"
-    (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++
-    spc () ++ str"It is corrupted" ++ spc () ++
-    str"or was compiled with another version of Coq.")
+let raw_intern_library f =
+  System.raw_intern_state Coq_config.vo_magic_number f
 
 (************************************************************************)
 (* Internalise libraries *)
 
 open Cic
 
-let mk_library md f table digest cst = {
-  library_name = md.md_name;
+let mk_library sd md f table digest cst = {
+  library_name = sd.md_name;
   library_filename = f;
   library_compiled = md.md_compiled;
   library_opaques = table;
-  library_deps = md.md_deps;
+  library_deps = sd.md_deps;
   library_digest = digest;
   library_extra_univs = cst }
 
@@ -310,10 +300,11 @@ let depgraph = ref LibraryMap.empty
 
 let intern_from_file (dir, f) =
   Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
-  let (md,table,opaque_csts,digest) =
+  let (sd,md,table,opaque_csts,digest) =
     try
-      let ch = with_magic_number_check raw_intern_library f in
-      let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
+      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 (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
@@ -325,9 +316,9 @@ let intern_from_file (dir, f) =
       if not (String.equal (Digest.channel ch pos) checksum) then
         errorlabstrm "intern_from_file" (str "Checksum mismatch");
       let () = close_in ch in
-      if dir <> md.md_name then
+      if dir <> sd.md_name then
         errorlabstrm "intern_from_file"
-          (name_clash_message dir md.md_name f);
+          (name_clash_message dir sd.md_name f);
       if tasks <> None || discharging <> None then
         errorlabstrm "intern_from_file"
           (str "The file "++str f++str " contains unfinished tasks");
@@ -340,25 +331,25 @@ let intern_from_file (dir, f) =
       Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
       end;
       (* Verification of the unmarshalled values *)
+      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 ();
       let digest =
         if opaque_csts <> None then Cic.Dviovo (digest,udg)
         else (Cic.Dvo digest) in
-      md,table,opaque_csts,digest
+      sd,md,table,opaque_csts,digest
     with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
-  depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
-  opaque_tables := LibraryMap.add md.md_name table !opaque_tables;
+  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,_,_) ->
     opaque_univ_tables :=
-      LibraryMap.add md.md_name opaque_csts !opaque_univ_tables)
+      LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables)
     opaque_csts;
   let extra_cst =
-    Option.default Univ.empty_constraint
-      (Option.map (fun (_,cs,_) ->
-         Univ.ContextSet.constraints cs) opaque_csts) in
-  mk_library md f table digest extra_cst
+    Option.default Univ.ContextSet.empty
+      (Option.map (fun (_,cs,_) -> cs) opaque_csts) in
+  mk_library sd md f table digest extra_cst
 
 let get_deps (dir, f) =
   try LibraryMap.find dir !depgraph
diff --git a/checker/check.mllib b/checker/check.mllib
index 22df3756..49ca6bf0 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,6 +1,7 @@
 Coq_config
 
 Hook
+Terminal
 Canary
 Hashset
 Hashcons
@@ -23,13 +24,14 @@ Pp
 Segmenttree
 Unicodetable
 Unicode
-Errors
 CObj
 CList
 CString
 CArray
 CStack
 Util
+Ppstyle
+Errors
 Ephemeron
 Future
 CUnix
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 05a2a1b9..d041f1b7 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -23,11 +23,17 @@ let print_memory_stat () =
 
 let output_context = ref false
 
-let pr_engt = function
-    Some ImpredicativeSet ->
-      str "Theory: Set is impredicative"
-  | None ->
-      str "Theory: Set is predicative"
+let pr_engagement (impr_set,type_in_type) =
+  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 =
   Cmap_env.fold
@@ -54,7 +60,7 @@ let print_context env =
     ppnl(hov 0
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
-      str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_ax csts) ++
       fnl())); pp_flush()
   end
diff --git a/checker/checker.ml b/checker/checker.ml
index 9a1007ac..d5d9b9e3 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -67,13 +67,13 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
       Check.add_load_path (dir,coq_dirpath)
     end
   else
-    msg_warning (str ("Cannot open " ^ dir))
+    msg_warning (str "Cannot open " ++ str dir)
 
 let convert_string d =
   try Id.of_string d
   with Errors.UserError _ ->
     if_verbose msg_warning
-      (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
+      (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
     raise Exit
 
 let add_rec_path ~unix_path ~coq_root =
@@ -90,7 +90,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 " ^ unix_path))
+    msg_warning (str "Cannot open " ++ str unix_path)
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
@@ -138,10 +138,11 @@ let init_load_path () =
 
 let set_debug () = Flags.debug := true
 
-let engagement = ref None
-let set_engagement c = engagement := Some c
-let engage () =
-  match !engagement with Some c -> Safe_typing.set_engagement c | None -> ()
+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 admit_list = ref ([] : section_path list)
@@ -194,6 +195,7 @@ 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"
@@ -221,7 +223,7 @@ let print_loc loc =
   else
     let loc = Loc.unloc loc in
     (int (fst loc) ++ str"-" ++ int (snd loc))
-let guill s = "\""^s^"\""
+let guill s = str "\"" ++ str s ++ str "\""
 
 let where s =
   if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
@@ -232,7 +234,7 @@ let rec explain_exn = function
   | Stream.Error txt ->
       hov 0 (str "Syntax error: " ++ str txt)
   | Sys_error msg ->
-      hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report() )
+      hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ guill msg ++ report() )
   | UserError(s,pps) ->
       hov 1 (str "User error: " ++ where s ++ pps)
   | Out_of_memory ->
@@ -241,14 +243,14 @@ let rec explain_exn = function
       hov 0 (str "Stack overflow")
   | Match_failure(filename,pos1,pos2) ->
       hov 1 (anomaly_string () ++ str "Match failure in file " ++
-	     str (guill filename) ++ str " at line " ++ int pos1 ++
+	     guill filename ++ str " at line " ++ int pos1 ++
 	     str " character " ++ int pos2 ++ report ())
   | Not_found ->
       hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ())
   | Failure s ->
       hov 0 (str "Failure: " ++ str s ++ report ())
   | Invalid_argument s ->
-      hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
+      hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ())
   | Sys.Break ->
       hov 0 (fnl () ++ str "User interrupt.")
   | Univ.UniverseInconsistency (o,u,v) ->
@@ -294,7 +296,7 @@ let rec explain_exn = function
           Format.printf "@\n====== universes ====@\n";
           Pp.pp (Univ.pr_universes
             (ctx.Environ.env_stratification.Environ.env_universes));
-          str("\nCantApplyBadType at argument " ^ string_of_int n)
+          str "\nCantApplyBadType at argument " ++ int n
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
       | IllFormedRecBody _ -> str"IllFormedRecBody"
       | IllTypedRecBody _ -> str"IllTypedRecBody"
@@ -309,7 +311,7 @@ let rec explain_exn = function
       hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
 	       (if s = "" then mt ()
 		else
-		  (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
+		  (str "(file \"" ++ str s ++ str "\", line " ++ int b ++
 		   str ", characters " ++ int e ++ str "-" ++
 		   int (e+6) ++ str ")")) ++
 	       report ())
@@ -319,11 +321,13 @@ let parse_args argv =
   let rec parse = function
     | [] -> ()
     | "-impredicative-set" :: rem ->
-      set_engagement Cic.ImpredicativeSet; parse 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 
-	fatal_error (str ("Directory '"^s^"' does not exist")) false;
+	fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false;
       Flags.coqlib := s;
       Flags.coqlib_spec := true;
       parse rem
diff --git a/checker/cic.mli b/checker/cic.mli
index 90a0e9fe..bd75111a 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -102,7 +102,7 @@ type constr =
   | Case      of case_info * constr * constr * constr array
   | Fix       of constr pfixpoint
   | CoFix     of constr pcofixpoint
-  | Proj      of constant * constr
+  | Proj      of projection * constr
 
 type existential = constr pexistential
 type rec_declaration = constr prec_declaration
@@ -165,7 +165,10 @@ type action
 
 (** Engagements *)
 
-type engagement = ImpredicativeSet
+type set_predicativity = ImpredicativeSet | PredicativeSet
+type type_hierarchy = TypeInType | StratifiedType
+
+type engagement = set_predicativity * type_hierarchy
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
@@ -377,7 +380,7 @@ and module_body =
     (** algebraic type, kept if it's relevant for extraction *)
     mod_type_alg : module_expression option;
     (** set of all constraints in the module  *)
-    mod_constraints : Univ.constraints;
+    mod_constraints : Univ.ContextSet.t;
     (** quotiented set of equivalent constants and inductive names *)
     mod_delta : delta_resolver;
     mod_retroknowledge : action list }
@@ -407,7 +410,7 @@ type compiled_library = {
   comp_name : compilation_unit_name;
   comp_mod : module_body;
   comp_deps : library_deps;
-  comp_enga : engagement option;
+  comp_enga : engagement;
   comp_natsymbs : nativecode_symb_array
 }
 
@@ -417,12 +420,16 @@ type compiled_library = {
 
 type library_objects
 
-type library_disk = {
+type summary_disk = {
   md_name : compilation_unit_name;
+  md_imports : compilation_unit_name array;
+  md_deps : library_deps;
+}
+
+type library_disk = {
   md_compiled : compiled_library;
   md_objects : library_objects;
-  md_deps : library_deps;
-  md_imports : compilation_unit_name array }
+}
 
 type opaque_table = constr Future.computation array
 type univ_table =
diff --git a/checker/closure.ml b/checker/closure.ml
index 356b683f..c6cc2185 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -276,7 +276,7 @@ and fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of constant * fconstr
+  | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCase of case_info * fconstr * fconstr * fconstr array
@@ -308,7 +308,7 @@ type stack_member =
   | Zapp of fconstr array
   | Zcase of case_info * fconstr * fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * constant
+  | Zproj of int * int * projection
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -678,8 +678,9 @@ let eta_expand_ind_stack env ind m s (f, s') =
       let (depth, args, s) = strip_update_shift_app m s in
       (** Try to drop the params, might fail on partially applied constructors. *)
       let argss = try_drop_parameters depth pars args in
-      let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
-					 term = FProj (p, right) }) projs in
+	let hstack =
+	  Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
+			     term = FProj (Projection.make p false, right) }) projs in
 	argss, [Zapp hstack]	
     | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
@@ -738,7 +739,7 @@ let rec knh info m stk =
     | FCast(t,_,_) -> knh info t stk
 
     | FProj (p,c) ->
-      if red_set info.i_flags (fCONST p) then
+      if red_set info.i_flags (fCONST (Projection.constant p)) then
         (let pb = lookup_projection p (info.i_env) in
 	   knh info c (Zproj (pb.proj_npars, pb.proj_arg, p)
 		       :: zupdate m stk))
diff --git a/checker/closure.mli b/checker/closure.mli
index e6b39250..376e9fef 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -95,7 +95,7 @@ type fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of constant * fconstr
+  | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCase of case_info * fconstr * fconstr * fconstr array
@@ -117,7 +117,7 @@ type stack_member =
   | Zapp of fconstr array
   | Zcase of case_info * fconstr * fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * constant
+  | Zproj of int * int * projection
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 8d913475..32d1713a 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -206,14 +206,15 @@ let rec map_kn f f' c =
   let func = map_kn f f' in
     match c with
       | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c)
-      | Proj (kn,t) -> 
-          let kn' = 
-	    try fst (f' kn Univ.Instance.empty)
-	    with No_subst -> kn 
+      | Proj (p,t) -> 
+          let p' = 
+	    Projection.map (fun kn ->
+			    try fst (f' kn Univ.Instance.empty)
+			    with No_subst -> kn) p
 	  in
 	  let t' = func t in
-	    if kn' == kn && t' == t then c
-	    else Proj (kn', t')
+	    if p' == p && t' == t then c
+	    else Proj (p', t')
       | Ind ((kn,i),u) ->
 	  let kn' = f kn in
 	  if kn'==kn then c else Ind ((kn',i),u)
@@ -425,7 +426,7 @@ let subst_lazy_constr sub = function
 let indirect_opaque_access =
   ref ((fun dp i -> assert false) : DirPath.t -> int -> constr)
 let indirect_opaque_univ_access =
-  ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.constraints)
+  ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.ContextSet.t)
 
 let force_lazy_constr = function
   | Indirect (l,dp,i) ->
@@ -434,7 +435,7 @@ let force_lazy_constr = function
 
 let force_lazy_constr_univs = function
   | OpaqueDef (Indirect (l,dp,i)) -> !indirect_opaque_univ_access dp i
-  | _ -> Univ.empty_constraint
+  | _ -> Univ.ContextSet.empty
 
 let subst_constant_def sub = function
   | Undef inl -> Undef inl
@@ -456,6 +457,8 @@ let is_opaque cb = match cb.const_body with
   | OpaqueDef _ -> true
   | Def _ | Undef _ -> false
 
+let opaque_univ_context cb = force_lazy_constr_univs cb.const_body
+
 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
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 3c6db6ab..456df836 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -2,17 +2,18 @@ open Names
 open Cic
 
 val force_constr : constr_substituted -> constr
-val force_lazy_constr_univs : Cic.constant_def -> Univ.constraints
+val force_lazy_constr_univs : Cic.constant_def -> Univ.ContextSet.t
 val from_val : constr -> constr_substituted
 
 val indirect_opaque_access : (DirPath.t -> int -> constr) ref
-val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.constraints) ref
+val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.ContextSet.t) ref
 
 (** Constant_body *)
 
 val body_of_constant : constant_body -> constr option
 val constant_has_body : constant_body -> bool
 val is_opaque : constant_body -> bool
+val opaque_univ_context : constant_body -> Univ.ContextSet.t
 
 (* Mutual inductives *)
 
diff --git a/checker/environ.ml b/checker/environ.ml
index 710ebc71..f8f5c29b 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -14,7 +14,7 @@ type globals = {
 
 type stratification = {
   env_universes : Univ.universes;
-  env_engagement : engagement option
+  env_engagement : engagement
 }
 
 type env = {
@@ -33,19 +33,28 @@ let empty_env = {
   env_rel_context = [];
   env_stratification =
   { env_universes = Univ.initial_universes;
-    env_engagement = None};
+    env_engagement = (PredicativeSet,StratifiedType)};
   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 c env =
-  match env.env_stratification.env_engagement with
-    | Some c' -> if c=c' then env else error "Incompatible engagement"
-    | None ->
-        { env with env_stratification =
-          { env.env_stratification with env_engagement = Some c } }
+let set_engagement (impr_set,type_in_type as c) env =
+  let expected_impr_set,expected_type_in_type =
+    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 } }
 
 (* Digests *)
 
@@ -75,13 +84,20 @@ let push_rec_types (lna,typarray,_) env =
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
 (* Universe constraints *)
-let add_constraints c env =
-  if c == Univ.Constraint.empty then
-    env
-  else
-    let s = env.env_stratification in
+let map_universes f env =
+  let s = env.env_stratification in
     { env with env_stratification =
-      { s with env_universes = Univ.merge_constraints c s.env_universes } }
+	 { s with env_universes = f s.env_universes } }
+
+let add_constraints c env =
+  if c == Univ.Constraint.empty then env
+  else map_universes (Univ.merge_constraints c) env
+			   
+let push_context ?(strict=false) ctx env =
+  map_universes (Univ.merge_context strict ctx) env
+
+let push_context_set ?(strict=false) ctx env =
+  map_universes (Univ.merge_context_set strict ctx) env
 
 let check_constraints cst env =
   Univ.check_constraints cst env.env_stratification.env_universes
@@ -147,8 +163,8 @@ let evaluable_constant cst env =
 let is_projection cst env = 
   not (Option.is_empty (lookup_constant cst env).const_proj)
 
-let lookup_projection cst env =
-  match (lookup_constant cst env).const_proj with 
+let lookup_projection p env =
+  match (lookup_constant (Projection.constant p) env).const_proj with 
   | Some pb -> pb
   | None -> anomaly ("lookup_projection: constant is not a projection")
 
diff --git a/checker/environ.mli b/checker/environ.mli
index d3448b12..87f143d1 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -11,7 +11,7 @@ type globals = {
   env_modtypes : module_type_body MPmap.t}
 type stratification = {
   env_universes : Univ.universes;
-  env_engagement : engagement option;
+  env_engagement : engagement;
 }
 type env = {
   env_globals : globals;
@@ -22,7 +22,7 @@ type env = {
 val empty_env : env
 
 (* Engagement *)
-val engagement : env -> Cic.engagement option
+val engagement : env -> Cic.engagement
 val set_engagement : Cic.engagement -> env -> env
 
 (* Digests *)
@@ -39,6 +39,8 @@ val push_rec_types : name array * constr array * 'a -> env -> env
 (* Universes *)
 val universes : env -> Univ.universes
 val add_constraints : Univ.constraints -> env -> env
+val push_context : ?strict:bool -> Univ.universe_context -> env -> env
+val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
 val check_constraints : Univ.constraints -> env -> bool
 
 (* Constants *)
@@ -51,7 +53,7 @@ val constant_value : env -> constant puniverses -> constr
 val evaluable_constant : constant -> env -> bool
 
 val is_projection : constant -> env -> bool
-val lookup_projection : constant -> env -> projection_body
+val lookup_projection : projection -> env -> projection_body
 
 (* Inductives *)
 val mind_equiv : env -> inductive -> inductive -> bool
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 050c33e6..f02f03dc 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, engagement env with
+  match s, fst (engagement env) with
       Type u, _ ->
         (* let u' = fresh_local_univ () in *)
         (* let cst = *)
@@ -184,7 +184,7 @@ let check_predicativity env s small level =
         (*     (universes env) in *)
         if not (Univ.check_leq (universes env) level u) then
           failwith "impredicative Type inductive type"
-    | Prop Pos, Some ImpredicativeSet -> ()
+    | Prop Pos, ImpredicativeSet -> ()
     | Prop Pos, _ ->
         if not small then failwith "impredicative Set inductive type"
     | Prop Null,_ -> ()
@@ -269,7 +269,7 @@ type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
   | LocalNotConstructor
-  | LocalNonPar of int * int
+  | LocalNonPar of int * int * int
 
 exception IllFormedInd of ill_formed_ind
 
@@ -291,9 +291,9 @@ let explain_ind_err ntyp env0 nbpar c err =
     | LocalNotConstructor ->
 	raise (InductiveError
 		 (NotConstructor (env,c',Rel (ntyp+nbpar))))
-    | LocalNonPar (n,l) ->
+    | LocalNonPar (n,i,l) ->
 	raise (InductiveError
-		 (NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar))))
+		 (NonPar (env,c',n,Rel i,Rel (l+nbpar))))
 
 let failwith_non_pos n ntypes c =
   for k = n to n + ntypes - 1 do
@@ -323,7 +323,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
     | _::hyps ->
         match whd_betadeltaiota env lpar.(k) with
 	  | Rel w when w = index -> check (k-1) (index+1) hyps
-	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
+	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l)))
   in check (nparams-1) (n-nhyps) hyps;
   if not (Array.for_all (noccur_between n ntypes) largs') then
     failwith_non_pos_vect n ntypes largs'
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 59d1a645..21b80f32 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -103,13 +103,12 @@ let instantiate_params full t u args sign =
 
 let full_inductive_instantiate mib u params sign =
   let dummy = Prop Null in
-  let t = mkArity (sign,dummy) in
+  let t = mkArity (subst_instance_context u sign,dummy) in
     fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
 
-let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
-  let inst_ind = constructor_instantiate mind u mib in
-  (fun t ->
-    instantiate_params true (inst_ind t) u params mib.mind_params_ctxt)
+let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
+  let inst_ind = constructor_instantiate mind u mib t in
+    instantiate_params true inst_ind u params mib.mind_params_ctxt
 
 (************************************************************************)
 (************************************************************************)
@@ -142,53 +141,60 @@ let sort_as_univ = function
 | Prop Null -> Univ.type0m_univ
 | Prop Pos -> Univ.type0_univ
 
+(* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
+(* in the domain or add [u |-> sup x su] if [u] is already mapped *)
+(* to [x]. *)
 let cons_subst u su subst =
-  Univ.LMap.add u su subst
-
-let actualize_decl_level env lev t =
-  let sign,s = dest_arity env t in
-  mkArity (sign,lev)
-
-let polymorphism_on_non_applied_parameters = false
+  try
+    Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+  with Not_found -> Univ.LMap.add u su subst
+
+(* remember_subst updates the mapping [u |-> x] by [u |-> sup x u] *)
+(* if it is presents and returns the substitution unchanged if not.*)
+let remember_subst u subst =
+  try
+    let su = Universe.make u in
+    Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+  with Not_found -> subst
 
 (* Bind expected levels of parameters to actual levels *)
 (* Propagate the new levels in the signature *)
-let rec make_subst env = function
-  | (_,Some _,_ as t)::sign, exp, args ->
-      let ctx,subst = make_subst env (sign, exp, args) in
-      t::ctx, subst
-  | d::sign, None::exp, args ->
-      let args = match args with _::args -> args | [] -> [] in
-      let ctx,subst = make_subst env (sign, exp, args) in
-      d::ctx, subst
-  | d::sign, Some u::exp, a::args ->
-      (* We recover the level of the argument, but we don't change the *)
-      (* level in the corresponding type in the arity; this level in the *)
-      (* arity is a global level which, at typing time, will be enforce *)
-      (* to be greater than the level of the argument; this is probably *)
-      (* a useless extra constraint *)
-      let s = sort_as_univ (snd (dest_arity env a)) in
-      let ctx,subst = make_subst env (sign, exp, args) in
-      d::ctx, cons_subst u s subst
-  | (na,None,t as d)::sign, Some u::exp, [] ->
-      (* No more argument here: we instantiate the type with a fresh level *)
-      (* which is first propagated to the corresponding premise in the arity *)
-      (* (actualize_decl_level), then to the conclusion of the arity (via *)
-      (* the substitution) *)
-      let ctx,subst = make_subst env (sign, exp, []) in
-	d::ctx, subst
-  | sign, [], _ ->
-      (* Uniform parameters are exhausted *)
-      sign,Univ.LMap.empty
-  | [], _, _ ->
-      assert false
-
+let rec make_subst env =
+  let rec make subst = function
+    | (_,Some _,_)::sign, exp, args ->
+        make subst (sign, exp, args)
+    | d::sign, None::exp, args ->
+        let args = match args with _::args -> args | [] -> [] in
+        make subst (sign, exp, args)
+    | d::sign, Some u::exp, a::args ->
+        (* We recover the level of the argument, but we don't change the *)
+        (* level in the corresponding type in the arity; this level in the *)
+        (* arity is a global level which, at typing time, will be enforce *)
+        (* to be greater than the level of the argument; this is probably *)
+        (* 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, [] ->
+        (* 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 *)
+        (* already in the domain of the substitution) [remember_subst] will *)
+        (* update its image [x] by [sup x u] in order not to forget the *)
+        (* dependency in [u] that remains to be fullfilled. *)
+        make (remember_subst u subst) (sign, exp, [])
+    | sign, [], _ ->
+        (* Uniform parameters are exhausted *)
+        subst
+    | [], _, _ ->
+        assert false
+  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 ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
+  let subst = make_subst env (ctx,ar.template_param_levels,args) in
   let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 998e23c6..3ea5ed0d 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -18,19 +18,27 @@ 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 u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in
-        mkArity (ctxt,Prop Null), 
-	  Univ.enforce_leq u u' Univ.empty_constraint
-    | _ -> ar, Univ.empty_constraint
+      let ul = Univ.Level.make empty_dirpath 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
+        mkArity (ctxt,Prop Null), ctx
+    | _ -> ar, Univ.ContextSet.empty
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn); pp_flush ();
-  let env' = add_constraints (Univ.UContext.constraints cb.const_universes) env in
+  let env' =
+    if cb.const_polymorphic then
+      let inst = Univ.make_abstract_instance cb.const_universes in
+      let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in
+        push_context ~strict:false ctx env
+    else push_context ~strict:true cb.const_universes env
+  in
   let envty, ty = 
     match cb.const_type with
       RegularArity ty ->
         let ty', cu = refresh_arity ty in
-        let envty = add_constraints cu env' in
+        let envty = push_context_set cu env' in
         let _ = infer_type envty ty' in envty, ty
     | TemplateArity(ctxt,par) ->
         let _ = check_ctxt env' ctxt in
@@ -69,7 +77,7 @@ let mk_mtb mp sign delta =
     mod_expr = Abstract;
     mod_type = sign;
     mod_type_alg = None;
-    mod_constraints = Univ.Constraint.empty;
+    mod_constraints = Univ.ContextSet.empty;
     mod_delta = delta;
     mod_retroknowledge = []; }
 
diff --git a/checker/modops.ml b/checker/modops.ml
index 8ccf118d..7f07f8bf 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -83,12 +83,13 @@ let strengthen_const mp_from l cb resolver =
     | Def _ -> cb
     | _ ->
       let con = Constant.make2 mp_from l in
-      (* let con =  constant_of_delta resolver con in*)
       let u = 
-	if cb.const_polymorphic then Univ.UContext.instance cb.const_universes 
+	if cb.const_polymorphic then
+	  Univ.make_abstract_instance cb.const_universes
 	else Univ.Instance.empty
       in
-      { cb with const_body = Def (Declarations.from_val (Const (con,u))) }
+      { cb with
+	const_body = Def (Declarations.from_val (Const (con,u))) }
 
 let rec strengthen_mod mp_from mp_to mb =
   if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb
diff --git a/checker/print.ml b/checker/print.ml
index 1cc48ff7..7624fd32 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -100,7 +100,7 @@ let print_pure_constr csr =
         done
       in print_string"{"; print_fix (); print_string"}"
   | Proj (p, c) ->
-    print_string "Proj("; sp_con_display p; print_string ","; 
+    print_string "Proj("; sp_con_display (Projection.constant p); print_string ","; 
     box_display c; print_string ")"
 
   and box_display c = open_hovbox 1; term_display c; close_box()
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 28fdb130..384d883e 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -52,7 +52,7 @@ let compare_stack_shape stk1 stk2 =
 
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
-  | Zlproj of Names.constant * lift
+  | Zlproj of Names.projection * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
   | Zlcase of case_info * lift * fconstr * fconstr array
 and lft_constr_stack = lft_constr_stack_elt list
@@ -137,7 +137,9 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
                 f fx1 fx2; cmp_rec a1 a2
 	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
-	      if not (Names.eq_con_chk c1 c2) then 
+	       if not (Names.eq_con_chk
+		       (Names.Projection.constant c1)
+		       (Names.Projection.constant c2)) then 
 		raise NotConvertible
             | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
                 if not (fmind ci1.ci_ind ci2.ci_ind) then
@@ -156,7 +158,7 @@ type conv_pb =
   | CONV
   | CUMUL
 
-let sort_cmp univ pb s0 s1 =
+let sort_cmp env univ pb s0 s1 =
   match (s0,s1) with
     | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible
     | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
@@ -165,14 +167,15 @@ let sort_cmp univ pb s0 s1 =
             CUMUL -> ()
           | _ -> raise NotConvertible)
     | (Type u1, Type u2) ->
-        if not
+        if snd (engagement env) == StratifiedType
+          && not
 	  (match pb with
             | CONV -> Univ.check_eq univ u1 u2
 	    | CUMUL -> Univ.check_leq univ u1 u2)
         then begin
           if !Flags.debug then begin
             let op = match pb with CONV -> "=" | CUMUL -> "<=" in
-            Printf.eprintf "cort_cmp: %s\n%!" Pp.(string_of_ppcmds
+            Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds
               (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
                ++ Univ.pr_universes univ))
           end;
@@ -259,7 +262,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
 	(match a1, a2 with
 	   | (Sort s1, Sort s2) ->
 	       assert (is_empty_stack v1 && is_empty_stack v2);
-	       sort_cmp univ cv_pb s1 s2
+	       sort_cmp (infos_env infos) univ cv_pb s1 s2
 	   | (Meta n, Meta m) ->
                if n=m
 	       then convert_stacks univ infos lft1 lft2 v1 v2
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 810d6e0b..81a3cc03 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -27,18 +27,26 @@ let set_engagement c =
 (* full_add_module adds module with universes and constraints *)
 let full_add_module dp mb univs digest =
   let env = !genv in
-  let env = add_constraints mb.mod_constraints env in
-  let env = add_constraints univs env in
+  let env = push_context_set ~strict:true mb.mod_constraints env in
+  let env = push_context_set ~strict:true univs env in
   let env = Modops.add_module mb env in
   genv := add_digest env dp digest
 
-(* Check that the engagement expected by a library matches the initial one *)
-let check_engagement env c =
-  match engagement env, c with
-    | Some ImpredicativeSet, Some ImpredicativeSet -> ()
-    | _, None -> ()
-    | _, Some ImpredicativeSet ->
-        error "Needs option -impredicative-set"
+(* 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
+  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 *)
 
@@ -75,8 +83,8 @@ let import file clib univs digest =
   check_engagement env clib.comp_enga;
   let mb = clib.comp_mod in
   Mod_checking.check_module
-    (add_constraints univs
-      (add_constraints mb.mod_constraints env)) mb.mod_mp mb;
+    (push_context_set ~strict:true univs
+      (push_context_set ~strict:true mb.mod_constraints env)) mb.mod_mp mb;
   stamp_library file digest;
   full_add_module clib.comp_name mb univs digest
 
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index e16e64e6..892a8d2c 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -15,6 +15,6 @@ val get_env : unit -> env
 
 val set_engagement : engagement -> unit
 val import         :
-  CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit
+  CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit
 val unsafe_import  :
-  CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit
+  CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit
diff --git a/checker/term.ml b/checker/term.ml
index 93540276..430be495 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -392,7 +392,7 @@ let compare_constr f t1 t2 =
       Array.equal f tl1 tl2 && Array.equal f bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
       Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
-  | Proj (p1,c1), Proj(p2,c2) -> eq_con_chk p1 p2 && f c1 c2
+  | Proj (p1,c1), Proj(p2,c2) -> Projection.equal p1 p2 && f c1 c2
   | _ -> false
 
 let rec eq_constr m n =
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 9bc4b269..21819992 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 engagement env = Some ImpredicativeSet then
+        if fst (engagement env) = ImpredicativeSet then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
         else
diff --git a/checker/univ.ml b/checker/univ.ml
index 3bcb3bc9..648e4781 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -244,7 +244,8 @@ module Level = struct
 
   let set = make Set
   let prop = make Prop
-
+  let var i = make (Var i)
+		  
   let is_small x = 
     match data x with
     | Level _ -> false
@@ -281,8 +282,8 @@ module Level = struct
 end
 
 (** Level sets and maps *)
-module LSet = Set.Make (Level)
-module LMap = Map.Make (Level)
+module LMap = HMap.Make (Level)
+module LSet = LMap.Set
 
 type 'a universe_map = 'a LMap.t
 
@@ -559,20 +560,26 @@ let repr g u =
   in
   repr_rec u
 
-(* [safe_repr] also search for the canonical representative, but
-   if the graph doesn't contain the searched universe, we add it. *)
-
-let safe_repr g u =
-  let rec safe_repr_rec u =
-    match UMap.find u g with
-      | Equiv v -> safe_repr_rec v
-      | Canonical arc -> arc
-  in
-  try g, safe_repr_rec u
-  with Not_found ->
-    let can = terminal u in
-    enter_arc can g, can
+let get_set_arc g = repr g Level.set
 
+exception AlreadyDeclared
+	    
+let add_universe vlev strict g =
+  try
+    let _arcv = UMap.find vlev g in
+      raise AlreadyDeclared
+  with Not_found -> 
+    let v = terminal vlev in
+    let arc =
+      let arc = get_set_arc g in
+	if strict then
+	  { arc with lt=vlev::arc.lt}
+	else 
+	  { arc with le=vlev::arc.le}
+    in
+    let g = enter_arc arc g in
+      enter_arc v g
+		       
 (* reprleq : canonical_arc -> canonical_arc list *)
 (* All canonical arcv such that arcu<=arcv with arcv#arcu *)
 let reprleq g arcu =
@@ -739,8 +746,8 @@ let is_lt g arcu arcv =
 (** First, checks on universe levels *)
 
 let check_equal g u v =
-  let g, arcu = safe_repr g u in
-  let _, arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
   arcu == arcv
 
 let check_eq_level g u v = u == v || check_equal g u v
@@ -749,8 +756,8 @@ let is_set_arc u = Level.is_set u.univ
 let is_prop_arc u = Level.is_prop u.univ
 
 let check_smaller g strict u v =
-  let g, arcu = safe_repr g u in
-  let g, arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
   if strict then
     is_lt g arcu arcv
   else
@@ -900,8 +907,8 @@ let error_inconsistency o u v =
 (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
 
 let enforce_univ_eq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastEQ -> g
     | FastLT -> error_inconsistency Eq v u
@@ -916,8 +923,8 @@ let enforce_univ_eq u v g =
 (* enforce_univ_leq : Level.t -> Level.t -> unit *)
 (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
 let enforce_univ_leq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
   if is_leq g arcu arcv then g
   else
     match fast_compare g arcv arcu with
@@ -928,8 +935,8 @@ let enforce_univ_leq u v g =
 
 (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
 let enforce_univ_lt u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastLT -> g
     | FastLE -> fst (setlt g arcu arcv)
@@ -941,7 +948,10 @@ let enforce_univ_lt u v g =
       | FastLE | FastLT -> error_inconsistency Lt u v
 
 (* Prop = Set is forbidden here. *)
-let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty
+let initial_universes =
+  let g = enter_arc (terminal Level.set) UMap.empty in
+  let g = enter_arc (terminal Level.prop) g in
+    enforce_univ_lt Level.prop Level.set g
 
 (* Constraints and sets of constraints. *)    
 
@@ -970,7 +980,7 @@ module Constraint = Set.Make(UConstraintOrd)
 let empty_constraint = Constraint.empty
 let merge_constraints c g =
   Constraint.fold enforce_constraint c g
-
+		  
 type constraints = Constraint.t
 
 (** A value with universe constraints. *)
@@ -1146,7 +1156,7 @@ struct
 
   (** Universe contexts (variables as a list) *)
   let empty = (Instance.empty, Constraint.empty)
-
+  let make x = x
   let instance (univs, cst) = univs
   let constraints (univs, cst) = cst
 end
@@ -1158,6 +1168,8 @@ struct
   type t = LSet.t constrained
   let empty = LSet.empty, Constraint.empty
   let constraints (_, cst) = cst
+  let levels (ctx, _) = ctx
+  let make ctx cst = (ctx, cst)
 end
 type universe_context_set = ContextSet.t
 
@@ -1207,6 +1219,9 @@ let subst_instance_constraints s csts =
     (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
     csts Constraint.empty 
 
+let make_abstract_instance (ctx, _) = 
+  Array.mapi (fun i l -> Level.var i) ctx
+
 (** Substitute instance inst for ctx in csts *)
 let instantiate_univ_context (ctx, csts) = 
   (ctx, subst_instance_constraints ctx csts)
@@ -1238,6 +1253,20 @@ let subst_univs_universe fn ul =
 	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u))
 	  substs nosubst
 
+let merge_context strict ctx g =
+  let g = Array.fold_left
+   (* Be lenient, module typing reintroduces universes and 
+      constraints due to includes *)
+	    (fun g v -> try add_universe v strict g with AlreadyDeclared -> g)
+	    g (UContext.instance ctx)
+  in merge_constraints (UContext.constraints ctx) g
+
+let merge_context_set strict ctx g =
+  let g = LSet.fold
+	    (fun v g -> try add_universe v strict g with AlreadyDeclared -> g)
+	    (ContextSet.levels ctx) g
+  in merge_constraints (ContextSet.constraints ctx) g
+
 (** Pretty-printing *)
 
 let pr_arc = function
diff --git a/checker/univ.mli b/checker/univ.mli
index 742ef91a..02c1bbdb 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -74,6 +74,13 @@ val check_eq : universe check_function
 (** The initial graph of universes: Prop < Set *)
 val initial_universes : universes
 
+(** Adds a universe to the graph, ensuring it is >= or > Set.
+   @raises AlreadyDeclared if the level is already declared in the graph. *)
+
+exception AlreadyDeclared
+
+val add_universe : universe_level -> bool -> universes -> universes
+
 (** {6 Constraints. } *)
 
 type constraint_type = Lt | Le | Eq
@@ -117,14 +124,14 @@ type univ_inconsistency = constraint_type * universe * universe
 exception UniverseInconsistency of univ_inconsistency
 
 val merge_constraints : constraints -> universes -> universes
-
+						    
 val check_constraints : constraints -> universes -> bool
 
 (** {6 Support for universe polymorphism } *)
 
 (** Polymorphic maps from universe levels to 'a *)
 module LMap : Map.S with type key = universe_level
-
+module LSet : CSig.SetS with type elt = universe_level
 type 'a universe_map = 'a LMap.t
 
 (** {6 Substitution} *)
@@ -177,7 +184,7 @@ sig
   type t
 
   val empty : t
-
+  val make : universe_instance constrained -> t
   val instance : t -> Instance.t
   val constraints : t -> constraints
 
@@ -186,6 +193,7 @@ end
 module ContextSet :
   sig 
     type t
+    val make : LSet.t -> constraints -> t
     val empty : t
     val constraints : t -> constraints
   end
@@ -193,6 +201,9 @@ module ContextSet :
 type universe_context = UContext.t
 type universe_context_set = ContextSet.t
 
+val merge_context : bool -> universe_context -> universes -> universes
+val merge_context_set : bool -> universe_context_set -> universes -> universes
+
 val empty_level_subst : universe_level_subst
 val is_empty_level_subst : universe_level_subst -> bool
 
@@ -219,6 +230,9 @@ val subst_instance_constraints : universe_instance -> constraints -> constraints
 val instantiate_univ_context : universe_context -> universe_context
 val instantiate_univ_constraints : universe_instance -> universe_context -> constraints
 
+(** Build the relative instance corresponding to the context *)
+val make_abstract_instance : universe_context -> universe_instance
+									    
 (** {6 Pretty-printing of universes. } *)
 
 val pr_universes : universes -> Pp.std_ppcmds
diff --git a/checker/values.ml b/checker/values.ml
index cf93466b..34de511c 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 0a174243f8b06535c9eecbbe8d339fe1 checker/cic.mli
+MD5 76312d06933f47498a1981a6261c9f75 checker/cic.mli
 
 *)
 
@@ -126,6 +126,7 @@ let v_caseinfo =
   v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
 
 let v_cast = v_enum "cast_kind" 4
+let v_proj = v_tuple "projection" [|v_cst; v_bool|]
 
 let rec v_constr =
   Sum ("constr",0,[|
@@ -145,7 +146,7 @@ let rec v_constr =
     [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
     [|v_fix|]; (* Fix *)
     [|v_cofix|]; (* CoFix *)
-    [|v_cst;v_constr|] (* Proj *)
+    [|v_proj;v_constr|] (* Proj *)
   |])
 
 and v_prec = Tuple ("prec_declaration",
@@ -192,7 +193,9 @@ let v_lazy_constr =
 
 (** kernel/declarations *)
 
-let v_engagement = v_enum "eng" 1
+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_pol_arity =
   v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
@@ -205,8 +208,10 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
 
 let v_projbody =
-  v_tuple "projection_body" [|v_cst;Int;Int;v_constr;v_tuple "proj_eta" [|v_constr;v_constr|];
-			      v_constr|]
+  v_tuple "projection_body"
+	  [|v_cst;Int;Int;v_constr;
+	    v_tuple "proj_eta" [|v_constr;v_constr|];
+	    v_constr|]
 
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
@@ -302,17 +307,17 @@ and v_impl =
 and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *)
 and v_module =
   Tuple ("module_body",
-         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|])
+         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
 and v_modtype =
   Tuple ("module_type_body",
-         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|])
+         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
 
 (** kernel/safe_typing *)
 
 let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
 let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
 let v_compiled_lib =
-  v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|]
+  v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|]
 
 (** Library objects *)
 
@@ -350,8 +355,11 @@ let v_stm_seg = v_pair v_tasks v_counters
 
 (** Toplevel structures in a vo (see Cic.mli) *)
 
+let v_libsum =
+  Tuple ("summary", [|v_dp;Array v_dp;v_deps|])
+
 let v_lib =
-  Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|])
+  Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
 
 let v_opaques = Array (v_computation v_constr)
 let v_univopaques =
diff --git a/checker/votour.ml b/checker/votour.ml
index 7c954d6f..4aecb28f 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -21,32 +21,91 @@ sig
   type obj
   val input : in_channel -> obj
   val repr : obj -> obj repr
-  val size : int list -> int
+  val size : obj -> int
 end
 
-module Repr : S =
+module ReprObj : S =
 struct
-  type obj = Obj.t
+  type obj = Obj.t * int list
 
   let input chan =
     let obj = input_value chan in
     let () = CObj.register_shared_size obj in
-    obj
+    (obj, [])
 
-  let repr obj =
+  let repr (obj, pos) =
     if Obj.is_block obj then
       let tag = Obj.tag obj in
       if tag = Obj.string_tag then STRING (Obj.magic obj)
       else if tag < Obj.no_scan_tag then
-        let data = Obj.dup obj in
-        let () = Obj.set_tag data 0 in
+        let init i = (Obj.field obj i, i :: pos) in
+        let data = Array.init (Obj.size obj) init in
         BLOCK (tag, Obj.magic data)
       else OTHER
     else INT (Obj.magic obj)
 
-  let size p = CObj.shared_size_of_pos p
+  let size (_, p) = CObj.shared_size_of_pos p
+end
+
+module ReprMem : S =
+struct
+  open Analyze
+
+  type obj = data
+
+  let memory = ref [||]
+  let sizes = ref [||]
+  (** size, in words *)
+
+  let ws = Sys.word_size / 8
+
+  let rec init_size seen = function
+  | Int _ | Atm _ | Fun _ -> 0
+  | Ptr p ->
+    if seen.(p) then 0
+    else
+      let () = seen.(p) <- true in
+      match (!memory).(p) with
+      | Struct (tag, os) ->
+        let fold accu o = accu + 1 + init_size seen o in
+        let size = Array.fold_left fold 1 os in
+        let () = (!sizes).(p) <- size in
+        size
+      | String s ->
+        let size = 2 + (String.length s / ws) in
+        let () = (!sizes).(p) <- size in
+        size
+
+  let size = function
+  | Int _ | Atm _ | Fun _ -> 0
+  | Ptr p -> (!sizes).(p)
+
+  let repr = function
+  | Int i -> INT i
+  | Atm t -> BLOCK (t, [||])
+  | Fun _ -> OTHER
+  | Ptr p ->
+    match (!memory).(p) with
+    | Struct (tag, os) -> BLOCK (tag, os)
+    | String s -> STRING s
+
+  let input ch =
+    let obj, mem = parse_channel ch in
+    let () = memory := mem in
+    let () = sizes := Array.make (Array.length mem) (-1) in
+    let seen = Array.make (Array.length mem) false in
+    let _ = init_size seen obj in
+    obj
+
 end
 
+module Visit (Repr : S) :
+sig
+  val init : unit -> unit
+  val visit : Values.value -> Repr.obj -> int list -> unit
+end =
+struct
+
 (** Name of a value *)
 
 let rec get_name ?(extra=false) = function
@@ -92,7 +151,7 @@ let rec get_details v o = match v, Repr.repr o with
 
 let node_info (v,o,p) =
   get_name ~extra:true v ^ get_details v o ^
-    " (size "^ string_of_int (Repr.size p)^"w)"
+    " (size "^ string_of_int (Repr.size o)^"w)"
 
 (** Children of a block : type, object, position.
     For lists, we collect all elements of the list at once *)
@@ -201,14 +260,49 @@ let rec visit v o pos =
   | Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos
   | Failure _ | Invalid_argument _ -> visit v o pos
 
+end
+
 (** Loading the vo *)
 
+type header = {
+  magic : string;
+  (** Magic number of the marshaller *)
+  length : int;
+  (** Size on disk in bytes *)
+  size32 : int;
+  (** Size in words when loaded on 32-bit systems *)
+  size64 : int;
+  (** Size in words when loaded on 64-bit systems *)
+  objects : int;
+  (** Number of blocks defined in the marshalled structure *)
+}
+
+let dummy_header = {
+  magic = "\000\000\000\000";
+  length = 0;
+  size32 = 0;
+  size64 = 0;
+  objects = 0;
+}
+
+let parse_header chan =
+  let magic = String.create 4 in
+  let () = for i = 0 to 3 do magic.[i] <- input_char chan done in
+  let length = input_binary_int chan in
+  let objects = input_binary_int chan in
+  let size32 = input_binary_int chan in
+  let size64 = input_binary_int chan in
+  { magic; length; size32; size64; objects }
+
 type segment = {
   name : string;
   mutable pos : int;
   typ : Values.value;
+  mutable header : header;
 }
 
+let make_seg name typ = { name; typ; pos = 0; header = dummy_header }
+
 let visit_vo f =
   Printf.printf "\nWelcome to votour !\n";
   Printf.printf "Enjoy your guided tour of a Coq .vo or .vi file\n";
@@ -216,12 +310,19 @@ let visit_vo f =
   Printf.printf
     "At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!";
   let segments = [|
-    {name="library"; pos=0; typ=Values.v_lib};
-    {name="univ constraints of opaque proofs"; pos=0;typ=Values.v_univopaques}; 
-    {name="discharging info"; pos=0; typ=Opt Any};
-    {name="STM tasks"; pos=0; typ=Opt Values.v_stm_seg};
-    {name="opaque proofs"; pos=0; typ=Values.v_opaques}; 
+    make_seg "summary" Values.v_libsum;
+    make_seg "library" Values.v_lib;
+    make_seg "univ constraints of opaque proofs" Values.v_univopaques;
+    make_seg "discharging info" (Opt Any);
+    make_seg "STM tasks" (Opt Values.v_stm_seg);
+    make_seg "opaque proofs" Values.v_opaques;
   |] in
+  let repr =
+    if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S)
+    (** On 32-bit machines, representation may exceed the max size of arrays *)
+  in
+  let module Repr = (val repr : S) in
+  let module Visit = Visit(Repr) in
   while true do
     let ch = open_in_bin f in
     let magic = input_binary_int ch in
@@ -229,21 +330,24 @@ let visit_vo f =
     for i=0 to Array.length segments - 1 do
       let pos = input_binary_int ch in
       segments.(i).pos <- pos_in ch;
+      let header = parse_header ch in
+      segments.(i).header <- header;
       seek_in ch pos;
       ignore(Digest.input ch);
     done;
     Printf.printf "The file has %d segments, choose the one to visit:\n"
       (Array.length segments);
-    Array.iteri (fun i { name; pos } ->
-      Printf.printf "  %d: %s, starting at byte %d\n" i name pos)
+    Array.iteri (fun i { name; pos; header } ->
+      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 () = init () in
-    visit segments.(seg).typ o []
+    let () = Visit.init () in
+    Visit.visit segments.(seg).typ o []
   done
 
 let main =