Imported Upstream version 8.8.2upstream/8.8.2

49 files changed, 1516 insertions, 1464 deletions

diff --git a/checker/Makefile b/checker/Makefile
deleted file mode 100644
index 2bcc9d36..00000000
--- a/checker/Makefile
+++ /dev/null
@@ -1,88 +0,0 @@
-OCAMLC=ocamlc
-OCAMLOPT=ocamlopt
-
-COQSRC=..
-
-MLDIRS=-I $(COQSRC)/config -I $(COQSRC)/lib -I $(COQSRC)/kernel -I +camlp4
-BYTEFLAGS=$(MLDIRS)
-OPTFLAGS=$(MLDIRS)
-
-CHECKERNAME=coqchk
-
-BINARIES=../bin/$(CHECKERNAME)$(EXE) ../bin/$(CHECKERNAME).opt$(EXE)
-MCHECKERLOCAL :=\
-  declarations.cmo environ.cmo \
-  closure.cmo reduction.cmo \
-  type_errors.cmo \
-  modops.cmo \
-  inductive.cmo typeops.cmo \
-  indtypes.cmo subtyping.cmo mod_checking.cmo \
-validate.cmo \
-  safe_typing.cmo check.cmo \
-  check_stat.cmo checker.cmo
-
-MCHECKER:=\
-  $(COQSRC)/config/coq_config.cmo \
-  $(COQSRC)/lib/pp_control.cmo $(COQSRC)/lib/pp.cmo $(COQSRC)/lib/compat.cmo \
-  $(COQSRC)/lib/util.cmo $(COQSRC)/lib/option.cmo $(COQSRC)/lib/hashcons.cmo \
-  $(COQSRC)/lib/system.cmo $(COQSRC)/lib/flags.cmo \
-  $(COQSRC)/lib/predicate.cmo $(COQSRC)/lib/rtree.cmo \
-  $(COQSRC)/kernel/names.cmo $(COQSRC)/kernel/univ.cmo \
-  $(COQSRC)/kernel/esubst.cmo term.cmo \
-  $(MCHECKERLOCAL)
-
-all: $(BINARIES)
-
-byte : ../bin/$(CHECKERNAME)$(EXE)
-opt : ../bin/$(CHECKERNAME).opt$(EXE)
-
-check.cma: $(MCHECKERLOCAL)
-	ocamlc $(BYTEFLAGS) -a -o $@ $(MCHECKER)
-
-check.cmxa: $(MCHECKERLOCAL:.cmo=.cmx)
-	ocamlopt $(OPTFLAGS) -a -o $@ $(MCHECKER:.cmo=.cmx)
-
-../bin/$(CHECKERNAME)$(EXE): check.cma
-	ocamlc $(BYTEFLAGS) -o $@ unix.cma gramlib.cma check.cma main.ml
-
-../bin/$(CHECKERNAME).opt$(EXE): check.cmxa
-	ocamlopt $(OPTFLAGS) -o $@ unix.cmxa gramlib.cmxa check.cmxa main.ml
-
-stats:
-	@echo STRUCTURE
-	@wc names.ml term.ml declarations.ml environ.ml type_errors.ml
-	@echo
-	@echo REDUCTION
-	@-wc esubst.ml closure.ml reduction.ml
-	@echo
-	@echo TYPAGE
-	@wc univ.ml inductive.ml indtypes.ml typeops.ml safe_typing.ml
-	@echo
-	@echo MODULES
-	@wc modops.ml subtyping.ml
-	@echo
-	@echo INTERFACE
-	@wc check*.ml main.ml 
-	@echo
-	@echo TOTAL
-	@wc *.ml | tail -1
-
-.SUFFIXES:.ml .mli .cmi .cmo .cmx
-
-.ml.cmo:
-	$(OCAMLC) -c $(BYTEFLAGS) $<
-
-.ml.cmx:
-	$(OCAMLOPT) -c $(OPTFLAGS) $<
-
-.mli.cmi:
-	$(OCAMLC) -c $(BYTEFLAGS) $<
-
-
-depend::
-	ocamldep *.ml* > .depend
-
-clean::
-	rm -f *.cm* *.o *.a *~ $(BINARIES)
-
--include .depend
diff --git a/checker/analyze.ml b/checker/analyze.ml
index c48b8301..7047d8a1 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -4,6 +4,7 @@ let prefix_small_block =         0x80
 let prefix_small_int =           0x40
 let prefix_small_string =        0x20
 
+[@@@ocaml.warning "-32"]
 let code_int8 =                  0x00
 let code_int16 =                 0x01
 let code_int32 =                 0x02
@@ -25,6 +26,7 @@ let code_infixpointer =          0x11
 let code_custom =                0x12
 let code_block64 =               0x13
 
+[@@@ocaml.warning "-37"]
 type code_descr =
 | CODE_INT8
 | CODE_INT16
@@ -53,6 +55,55 @@ let magic_number = "\132\149\166\190"
 
 (** Memory reification *)
 
+module LargeArray :
+sig
+  type 'a t
+  val empty : 'a t
+  val length : 'a t -> int
+  val make : int -> 'a -> 'a t
+  val get : 'a t -> int -> 'a
+  val set : 'a t -> int -> 'a -> unit
+end =
+struct
+
+  let max_length = Sys.max_array_length
+
+  type 'a t = 'a array array * 'a array
+  (** Invariants:
+      - All subarrays of the left array have length [max_length].
+      - The right array has length < [max_length].
+  *)
+
+  let empty = [||], [||]
+
+  let length (vl, vr) =
+    (max_length * Array.length vl) + Array.length vr
+
+  let make n x =
+    let k = n / max_length in
+    let r = n mod max_length in
+    let vl = Array.init k (fun _ -> Array.make max_length x) in
+    let vr = Array.make r x in
+    (vl, vr)
+
+  let get (vl, vr) n =
+    let k = n / max_length in
+    let r = n mod max_length in
+    let len = Array.length vl in
+    if k < len then vl.(k).(r)
+    else if k == len then vr.(r)
+    else invalid_arg "index out of bounds"
+
+  let set (vl, vr) n x =
+    let k = n / max_length in
+    let r = n mod max_length in
+    let len = Array.length vl in
+    if k < len then vl.(k).(r) <- x
+    else if k == len then vr.(r) <- x
+    else invalid_arg "index out of bounds"
+
+end
+
 type repr =
 | RInt of int
 | RBlock of (int * int) (* tag × len *)
@@ -80,7 +131,7 @@ end
 module type S =
 sig
   type input
-  val parse : input -> (data * obj array)
+  val parse : input -> (data * obj LargeArray.t)
 end
 
 module Make(M : Input) =
@@ -101,11 +152,11 @@ let input_binary_int chan =
   input_binary_int chan
 
 let input_char chan = Char.chr (input_byte chan)
+let input_string len chan = String.init len (fun _ -> input_char 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 magic = input_string 4 chan in
   let length = input_binary_int chan in
   let objects = input_binary_int chan in
   let size32 = input_binary_int chan in
@@ -204,13 +255,6 @@ let input_header64 chan =
   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
@@ -251,7 +295,7 @@ let parse_object chan =
     RString (input_string len chan)
   | CODE_CODEPOINTER ->
     let addr = input_int32u chan in
-    for i = 0 to 15 do ignore (input_byte chan); done;
+    for _i = 0 to 15 do ignore (input_byte chan); done;
     RCode addr
   | CODE_DOUBLE_ARRAY32_LITTLE
   | CODE_DOUBLE_BIG
@@ -266,7 +310,7 @@ let parse_object chan =
 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 memory = LargeArray.make size (Struct ((-1), [||])) in
   let current_object = ref 0 in
   let fill_obj = function
   | RPointer n ->
@@ -277,7 +321,7 @@ let parse chan =
     data, None
   | RString s ->
     let data = Ptr !current_object in
-    let () = memory.(!current_object) <- String s in
+    let () = LargeArray.set memory !current_object (String s) in
     let () = incr current_object in
     data, None
   | RBlock (tag, 0) ->
@@ -287,7 +331,7 @@ let parse chan =
   | 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 () = LargeArray.set memory !current_object (Struct (tag, nblock)) in
     let () = incr current_object in
     data, Some nblock
   | RCode addr ->
@@ -348,3 +392,32 @@ module PString = Make(IString)
 
 let parse_channel = PChannel.parse
 let parse_string s = PString.parse (s, ref 0)
+
+let instantiate (p, mem) =
+  let len = LargeArray.length mem in
+  let ans = LargeArray.make len (Obj.repr 0) in
+  (** First pass: initialize the subobjects *)
+  for i = 0 to len - 1 do
+    let obj = match LargeArray.get mem i with
+    | Struct (tag, blk) -> Obj.new_block tag (Array.length blk)
+    | String str -> Obj.repr str
+    in
+    LargeArray.set ans i obj
+  done;
+  let get_data = function
+  | Int n -> Obj.repr n
+  | Ptr p -> LargeArray.get ans p
+  | Atm tag -> Obj.new_block tag 0
+  | Fun _ -> assert false (** We shouldn't serialize closures *)
+  in
+  (** Second pass: set the pointers *)
+  for i = 0 to len - 1 do
+    match LargeArray.get mem i with
+    | Struct (_, blk) ->
+      let obj = LargeArray.get ans i in
+      for k = 0 to Array.length blk - 1 do
+        Obj.set_field obj k (get_data blk.(k))
+      done
+    | String _ -> ()
+  done;
+  get_data p
diff --git a/checker/analyze.mli b/checker/analyze.mli
index 42efcf01..9c837643 100644
--- a/checker/analyze.mli
+++ b/checker/analyze.mli
@@ -8,8 +8,20 @@ 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)
+module LargeArray :
+sig
+  type 'a t
+  val empty : 'a t
+  val length : 'a t -> int
+  val make : int -> 'a -> 'a t
+  val get : 'a t -> int -> 'a
+  val set : 'a t -> int -> 'a -> unit
+end
+(** A data structure similar to arrays but allowing to overcome the 2^22 length
+    limitation on 32-bit architecture. *)
+
+val parse_channel : in_channel -> (data * obj LargeArray.t)
+val parse_string : string -> (data * obj LargeArray.t)
 
 (** {6 Functorized version} *)
 
@@ -26,10 +38,13 @@ end
 module type S =
 sig
   type input
-  val parse : input -> (data * obj array)
+  val parse : input -> (data * obj LargeArray.t)
   (** 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. *)
+
+val instantiate : data * obj LargeArray.t -> Obj.t
+(** Create the OCaml object out of the reified representation. *)
diff --git a/checker/check.ml b/checker/check.ml
index 8b299bf2..4bb485d2 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Pp
@@ -22,6 +24,11 @@ let extend_dirpath p id = DirPath.make (id :: DirPath.repr p)
 type section_path = {
   dirpath : string list ;
   basename : string }
+
+type object_file =
+| PhysicalFile of CUnix.physical_path
+| LogicalFile of section_path
+
 let dir_of_path p =
   DirPath.make (List.map Id.of_string p.dirpath)
 let path_of_dirpath dir =
@@ -69,11 +76,6 @@ let libraries_table = ref LibraryMap.empty
 let find_library dir =
   LibraryMap.find dir !libraries_table
 
-let try_find_library dir =
-  try find_library dir
-  with Not_found ->
-    error ("Unknown library " ^ (DirPath.to_string dir))
-
 let library_full_filename dir = (find_library dir).library_filename
 
   (* If a library is loaded several time, then the first occurrence must
@@ -129,8 +131,6 @@ type logical_path = DirPath.t
 
 let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list)
 
-let get_load_paths () = fst !load_paths
-
 (* Hints to partially detects if two paths refer to the same repertory *)
 let rec remove_path_dot p =
   let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
@@ -165,7 +165,7 @@ let find_logical_path phys_dir =
   match List.filter2 (fun p d -> p = phys_dir) physical logical with
   | _,[dir] -> dir
   | _,[] -> default_root_prefix
-  | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir))
+  | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir^"."))
 
 let remove_load_path dir =
   let physical, logical = !load_paths in
@@ -197,7 +197,7 @@ let add_load_path (phys_path,coq_path) =
 	    end
       | _,[] ->
 	  load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
-      | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path))
+      | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path^"."))
 
 let load_paths_of_dir_path dir =
   let physical, logical = !load_paths in
@@ -227,13 +227,8 @@ let locate_absolute_library dir =
 
 let locate_qualified_library qid =
   try
-    let loadpath =
-      (* Search library in loadpath *)
-      if qid.dirpath=[] then get_load_paths ()
-      else
-        (* we assume qid is an absolute dirpath *)
-        load_paths_of_dir_path (dir_of_path qid)
-    in
+    (* we assume qid is an absolute dirpath *)
+    let loadpath = load_paths_of_dir_path (dir_of_path qid) in
     if loadpath = [] then raise LibUnmappedDir;
     let name =  qid.basename^".vo" in
     let path, file = System.where_in_path loadpath name in
@@ -248,12 +243,12 @@ let locate_qualified_library qid =
 
 let error_unmapped_dir qid =
   let prefix = qid.dirpath in
-  errorlabstrm "load_absolute_library_from"
+  user_err ~hdr:"load_absolute_library_from"
     (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++
      str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ())
 
 let error_lib_not_found qid =
-  errorlabstrm "load_absolute_library_from"
+  user_err ~hdr:"load_absolute_library_from"
     (str"Cannot find library " ++ pr_path qid ++ str" in loadpath")
 
 let try_locate_absolute_library dir =
@@ -263,7 +258,17 @@ let try_locate_absolute_library dir =
     | LibUnmappedDir -> error_unmapped_dir (path_of_dirpath dir)
     | LibNotFound -> error_lib_not_found (path_of_dirpath dir)
 
-let try_locate_qualified_library qid =
+let try_locate_qualified_library lib = match lib with
+| PhysicalFile f ->
+  let () =
+    if not (System.file_exists_respecting_case "" f) then
+      error_lib_not_found { dirpath = []; basename = f; }
+  in
+  let dir = Filename.dirname f in
+  let base = Filename.chop_extension (Filename.basename f) in
+  let dir = extend_dirpath (find_logical_path dir) (Id.of_string base) in
+  (dir, f)
+| LogicalFile qid ->
   try
     locate_qualified_library qid
   with
@@ -298,34 +303,43 @@ let name_clash_message dir mdir f =
 (* Dependency graph *)
 let depgraph = ref LibraryMap.empty
 
+let marshal_in_segment f ch =
+  try
+    let stop = input_binary_int ch in
+    let v = Analyze.instantiate (Analyze.parse_channel ch) in
+    let digest = Digest.input ch in
+    Obj.obj v, stop, digest
+  with _ ->
+    user_err (str "Corrupted file " ++ quote (str f))
+
 let intern_from_file (dir, f) =
   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), _, 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
+      let (sd:Cic.summary_disk), _, digest = marshal_in_segment f ch in
+      let (md:Cic.library_disk), _, digest = marshal_in_segment f ch in
+      let (opaque_csts:'a option), _, udg = marshal_in_segment f ch in
+      let (discharging:'a option), _, _ = marshal_in_segment f ch in
+      let (tasks:'a option), _, _ = marshal_in_segment f ch in
       let (table:Cic.opaque_table), pos, checksum =
-        System.marshal_in_segment f ch in
+        marshal_in_segment f ch in
       (* Verification of the final checksum *)
       let () = close_in ch in
       let ch = open_in_bin f in
       if not (String.equal (Digest.channel ch pos) checksum) then
-        errorlabstrm "intern_from_file" (str "Checksum mismatch");
+        user_err ~hdr:"intern_from_file" (str "Checksum mismatch");
       let () = close_in ch in
       if dir <> sd.md_name then
-        errorlabstrm "intern_from_file"
+        user_err ~hdr:"intern_from_file"
           (name_clash_message dir sd.md_name f);
       if tasks <> None || discharging <> None then
-        errorlabstrm "intern_from_file"
+        user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
        chk_pp (str " (was a vio file) ");
       Option.iter (fun (_,_,b) -> if not b then
-        errorlabstrm "intern_from_file"
+        user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " is still a .vio"))
         opaque_csts;
       Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
@@ -412,9 +426,3 @@ let recheck_library ~norec ~admit ~check =
     (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
   List.iter (check_one_lib nochk) needed;
   Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked")
-
-open Printf
-
-let mem s =
-  let m = try_find_library s in
-  h 0 (str (sprintf "%dk" (CObj.size_kb m)))
diff --git a/checker/check.mli b/checker/check.mli
new file mode 100644
index 00000000..eb6404a1
--- /dev/null
+++ b/checker/check.mli
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open CUnix
+open Names
+
+type section_path = {
+  dirpath : string list;
+  basename : string;
+}
+
+type object_file =
+| PhysicalFile of physical_path
+| LogicalFile of section_path
+
+type logical_path = DirPath.t
+
+val default_root_prefix : DirPath.t
+
+val add_load_path : physical_path * logical_path -> unit
+
+val recheck_library :
+  norec:object_file list ->
+  admit:object_file list ->
+  check:object_file list -> unit
diff --git a/checker/check.mllib b/checker/check.mllib
index 488507a1..f79ba66e 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,5 +1,6 @@
 Coq_config
 
+Analyze
 Hook
 Terminal
 Canary
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 741f5328..3f00f924 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Pp
diff --git a/checker/check_stat.mli b/checker/check_stat.mli
index 39e19d10..823b107f 100644
--- a/checker/check_stat.mli
+++ b/checker/check_stat.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 val memory_stat : bool ref
diff --git a/checker/checker.ml b/checker/checker.ml
index 8dbb7e01..fd2725c8 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -1,25 +1,26 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Pp
 open CErrors
 open Util
 open System
-open Flags
 open Names
 open Check
 
 let () = at_exit flush_all
 
-let chk_pp = Pp.pp_with Format.std_formatter
+let pp_arrayi pp fmt a = Array.iteri (fun i x -> pp fmt (i,x)) a
 
 let fatal_error info anomaly =
-  flush_all (); Feedback.msg_error info; flush_all ();
+  flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]@\n%!" Pp.pp_with info; flush_all ();
   exit (if anomaly then 129 else 1)
 
 let coq_root = Id.of_string "Coq"
@@ -41,9 +42,10 @@ let dirpath_of_string s =
       [] -> Check.default_root_prefix
     | dir -> DirPath.make (List.map Id.of_string dir)
 let path_of_string s =
-  match parse_dir s with
+  if Filename.check_suffix s ".vo" then PhysicalFile s
+  else match parse_dir s with
       [] -> invalid_arg "path_of_string"
-    | l::dir -> {dirpath=dir; basename=l}
+    | l::dir -> LogicalFile {dirpath=dir; basename=l}
 
 let ( / ) = Filename.concat
 
@@ -74,7 +76,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
 let convert_string d =
   try Id.of_string d
   with CErrors.UserError _ ->
-    if_verbose Feedback.msg_warning
+    Flags.if_verbose Feedback.msg_warning
       (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
     raise Exit
 
@@ -96,17 +98,13 @@ let add_rec_path ~unix_path ~coq_root =
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
-let push_include (s, alias) = includes := (s,alias,false) :: !includes
-let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
+let push_include (s, alias) = includes := (s,alias) :: !includes
 
 let set_default_include d =
   push_include (d, Check.default_root_prefix)
 let set_include d p =
   let p = dirpath_of_string p in
   push_include (d,p)
-let set_rec_include d p =
-  let p = dirpath_of_string p in
-  push_rec_include(d,p)
 
 (* Initializes the LoadPath *)
 let init_load_path () =
@@ -132,8 +130,7 @@ let init_load_path () =
   add_path ~unix_path:"." ~coq_root:Check.default_root_prefix;
   (* additional loadpath, given with -I -include -R options *)
   List.iter
-    (fun (unix_path, coq_root, reci) ->
-      if reci then add_rec_path ~unix_path ~coq_root else add_path ~unix_path ~coq_root)
+    (fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root)
     (List.rev !includes);
   includes := []
 
@@ -145,15 +142,15 @@ let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet
 let engage () = Safe_typing.set_engagement (!impredicative_set)
 
 
-let admit_list = ref ([] : section_path list)
+let admit_list = ref ([] : object_file list)
 let add_admit s =
   admit_list := path_of_string s :: !admit_list
 
-let norec_list = ref ([] : section_path list)
+let norec_list = ref ([] : object_file list)
 let add_norec s =
   norec_list := path_of_string s :: !norec_list
 
-let compile_list = ref ([] : section_path list)
+let compile_list = ref ([] : object_file list)
 let add_compile s =
   compile_list := path_of_string s :: !compile_list
 
@@ -179,7 +176,9 @@ let print_usage_channel co command =
   output_string co command;
   output_string co "coqchk options are:\n";
   output_string co
-"  -R dir coqdir          map physical dir to logical coqdir\
+"  -Q dir coqdir          map physical dir to logical coqdir\
+\n  -R dir coqdir          synonymous for -Q\
+\n\
 \n\
 \n  -admit module          load module and dependencies without checking\
 \n  -norec module          check module but admit dependencies without checking\
@@ -211,15 +210,16 @@ let usage () =
 open Type_errors
 
 let anomaly_string () = str "Anomaly: "
-let report () = (str "." ++ spc () ++ str "Please report" ++
-                 strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".")
+let report () = strbrk (". Please report at " ^ Coq_config.wwwbugtracker ^ ".")
 
 let guill s = str "\"" ++ str s ++ str "\""
 
-let where s =
+let where = function
+| None -> mt ()
+| Some s ->
   if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
 
-let rec explain_exn = function
+let explain_exn = function
   | Stream.Failure ->
       hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
   | Stream.Error txt ->
@@ -269,26 +269,26 @@ let rec explain_exn = function
       | Generalization _ -> str"Generalization"
       | ActualType _ -> str"ActualType"
       | CantApplyBadType ((n,a,b),(hd,hdty),args) ->
-          Format.printf "====== ill-typed term ====@\n";
-          Format.printf "@[<hov 2>application head=@ ";
-          Print.print_pure_constr hd;
-          Format.printf "@]@\n@[<hov 2>head type=@ ";
-          Print.print_pure_constr hdty;
-          Format.printf "@]@\narguments:@\n@[<hv>";
-          Array.iteri (fun i (t,ty) ->
-            Format.printf "@[<hov 2>arg %d=@ " (i+1);
-            Print.print_pure_constr t;
-            Format.printf "@ type=@ ";
-            Print.print_pure_constr ty) args;
-          Format.printf "@]@\n====== type error ====@\n";
-          Print.print_pure_constr b;
-          Format.printf "@\nis not convertible with@\n";
-          Print.print_pure_constr a;
-          Format.printf "@\n====== universes ====@\n";
-          chk_pp
-            (Univ.pr_universes
-            (ctx.Environ.env_stratification.Environ.env_universes));
-          str "\nCantApplyBadType at argument " ++ int n
+        (* This mix of printf / pp was here before... *)
+        let fmt = Format.std_formatter in
+        let open Format in
+        let open Print in
+        fprintf fmt "====== ill-typed term ====@\n";
+        fprintf fmt "@[<hov 2>application head=@ %a@]@\n" print_pure_constr hd;
+        fprintf fmt "@[<hov 2>head type=@ %a@]@\n" print_pure_constr hdty;
+        let pp_arg fmt (i,(t,ty)) = fprintf fmt "@[<hv>@[<1>arg %d=@ @[%a@]@]@,@[<1>type=@ @[%a@]@]@]@\n@," (i+1)
+            print_pure_constr t print_pure_constr ty
+        in
+        fprintf fmt "arguments:@\n@[<hv>%a@]@\n" (pp_arrayi pp_arg) args;
+        fprintf fmt "====== type error ====@\n";
+        fprintf fmt "%a@\n" print_pure_constr b;
+        fprintf fmt "is not convertible with@\n";
+        fprintf fmt "%a@\n" print_pure_constr a;
+        fprintf fmt "====== universes ====@\n";
+        fprintf fmt "%a@\n%!" Pp.pp_with
+          (Univ.pr_universes
+             (ctx.Environ.env_stratification.Environ.env_universes));
+        str "CantApplyBadType at argument " ++ int n
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
       | IllFormedRecBody _ -> str"IllFormedRecBody"
       | IllTypedRecBody _ -> str"IllTypedRecBody"
@@ -309,6 +309,9 @@ let rec explain_exn = function
 	       report ())
   | e -> CErrors.print e (* for anomalies and other uncaught exceptions *)
 
+let deprecated flag =
+  Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag))
+
 let parse_args argv =
   let rec parse = function
     | [] -> ()
@@ -322,25 +325,28 @@ let parse_args argv =
       Flags.coqlib_spec := true;
       parse rem
 
-    | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
+    | ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem
     | ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
-    | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
+    | ("-I"|"-include") :: d :: rem -> deprecated "-I"; set_default_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
 
-    | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem
+    | "-Q" :: d :: p :: rem -> set_include d p;parse rem
+    | "-Q" :: ([] | [_]) -> usage ()
+
+    | "-R" :: d :: p :: rem -> set_include d p;parse rem
     | "-R" :: ([] | [_]) -> usage ()
 
     | "-debug" :: rem -> set_debug (); parse rem
 
     | "-where" :: _ ->
-        Envars.set_coqlib ~fail:CErrors.error;
+        Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
         print_endline (Envars.coqlib ());
         exit 0
 
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
 
     | ("-v"|"--version") :: _ -> version ()
-    | "-boot" :: rem -> boot := true; parse rem
+    | "-boot" :: rem -> Flags.boot := true; parse rem
     | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem
     | ("-o" | "--output-context") :: rem ->
         Check_stat.output_context := true; parse rem
@@ -352,7 +358,7 @@ let parse_args argv =
     | "-norec" :: [] -> usage ()
 
     | "-silent" :: rem ->
-        Flags.make_silent true; parse rem
+        Flags.quiet := true; parse rem
 
     | s :: _ when s<>"" && s.[0]='-' ->
         fatal_error (str "Unknown option " ++ str s) false
@@ -364,15 +370,18 @@ let parse_args argv =
 (* To prevent from doing the initialization twice *)
 let initialized = ref false
 
+(* XXX: At some point we need to either port the checker to use the
+   feedback system or to remove its use completely. *)
 let init_with_argv argv =
   if not !initialized then begin
     initialized := true;
     Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
+    let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
     try
       parse_args argv;
       if !Flags.debug then Printexc.record_backtrace true;
-      Envars.set_coqlib ~fail:CErrors.error;
-      if_verbose print_header ();
+      Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
+      Flags.if_verbose print_header ();
       init_load_path ();
       engage ();
     with e ->
diff --git a/checker/checker.mli b/checker/checker.mli
new file mode 100644
index 00000000..582f4258
--- /dev/null
+++ b/checker/checker.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val start : unit -> unit
diff --git a/checker/cic.mli b/checker/cic.mli
index 36455875..c4b00d0d 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Type definitions for the Calculus of Inductive Constructions *)
@@ -81,7 +83,7 @@ type 'constr pfixpoint =
 type 'constr pcofixpoint =
     int * 'constr prec_declaration
 type 'a puniverses = 'a Univ.puniverses
-type pconstant = constant puniverses
+type pconstant = Constant.t puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
@@ -102,7 +104,7 @@ type constr =
   | Case      of case_info * constr * constr * constr array
   | Fix       of constr pfixpoint
   | CoFix     of constr pcofixpoint
-  | Proj      of projection * constr
+  | Proj      of Projection.t * constr
 
 type existential = constr pexistential
 type rec_declaration = constr prec_declaration
@@ -127,12 +129,12 @@ type section_context = unit
 
 type delta_hint =
   | Inline of int * constr option
-  | Equiv of kernel_name
+  | Equiv of KerName.t
 
-type delta_resolver = module_path MPmap.t * delta_hint KNmap.t
+type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t
 
 type 'a umap_t = 'a MPmap.t * 'a MBImap.t
-type substitution = (module_path * delta_resolver) umap_t
+type substitution = (ModPath.t * delta_resolver) umap_t
 
 (** {6 Delayed constr} *)
 
@@ -170,6 +172,17 @@ type set_predicativity = ImpredicativeSet | PredicativeSet
 
 type engagement = set_predicativity
 
+(** {6 Conversion oracle} *)
+
+type level = Expand | Level of int | Opaque
+
+type oracle = {
+  var_opacity : level Id.Map.t;
+  cst_opacity : level Cmap.t;
+  var_trstate : Id.Pred.t;
+  cst_trstate : Cpred.t;
+}
+
 (** {6 Representation of constants (Definition/Axiom) } *)
 
 
@@ -182,8 +195,6 @@ type ('a, 'b) declaration_arity =
   | RegularArity of 'a
   | TemplateArity of 'b
 
-type constant_type = (constr, rel_context * template_arity) declaration_arity
-
 (** Inlining level of parameters at functor applications.
     This is ignored by the checker. *)
 
@@ -196,7 +207,7 @@ type inline = int option
     always transparent. *)
 
 type projection_body = {
-  proj_ind : mutual_inductive;
+  proj_ind : MutInd.t;
   proj_npars : int;
   proj_arg : int;
   proj_type : constr; (* Type under params *)
@@ -209,7 +220,9 @@ type constant_def =
   | Def of constr_substituted
   | OpaqueDef of lazy_constr
 
-type constant_universes = Univ.universe_context
+type constant_universes =
+  | Monomorphic_const of Univ.ContextSet.t
+  | Polymorphic_const of Univ.abstract_universe_context
 
 (** The [typing_flags] are instructions to the type-checker which
     modify its behaviour. The typing flags used in the type-checking
@@ -219,14 +232,14 @@ 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 *)
+  conv_oracle : oracle; (** Unfolding strategies for conversion *)
 }
 
 type constant_body = {
     const_hyps : section_context; (** New: younger hyp at top *)
     const_body : constant_def;
-    const_type : constant_type;
+    const_type : constr;
     const_body_code : to_patch_substituted;
-    const_polymorphic : bool; (** Is it polymorphic or not *)
     const_universes : constant_universes;
     const_proj : projection_body option;
     const_inline_code : bool;
@@ -242,7 +255,7 @@ type recarg =
 
 type wf_paths = recarg Rtree.t
 
-type record_body = (Id.t * constant array * projection_body array) option
+type record_body = (Id.t * Constant.t array * projection_body array) option
     (* The body is empty for non-primitive records, otherwise we get its
        binder name in projections and list of projections if it is primitive. *)
 
@@ -303,6 +316,11 @@ type one_inductive_body = {
     mind_reloc_tbl : reloc_table;
   }
 
+type abstract_inductive_universes =
+  | Monomorphic_ind of Univ.ContextSet.t
+  | Polymorphic_ind of Univ.abstract_universe_context
+  | Cumulative_ind of Univ.abstract_cumulativity_info
+
 type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
@@ -321,9 +339,7 @@ type mutual_inductive_body = {
 
     mind_params_ctxt : rel_context;  (** The context of parameters (includes let-in declaration) *)
 
-    mind_polymorphic : bool; (** Is it polymorphic or not *)
-
-    mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
+    mind_universes : abstract_inductive_universes; (** Local universe variables and constraints together with subtyping constraints *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
@@ -344,13 +360,11 @@ type ('ty,'a) functorize =
     and won't play any role into the kernel after that : they are kept
     only for short module printing and for extraction. *)
 
-type with_declaration =
-  | WithMod of Id.t list * module_path
-  | WithDef of Id.t list * (constr * Univ.universe_context)
+type with_declaration
 
 type module_alg_expr =
-  | MEident of module_path
-  | MEapply of module_alg_expr * module_path
+  | MEident of ModPath.t
+  | MEapply of module_alg_expr * ModPath.t
   | MEwith of module_alg_expr * with_declaration
 
 (** A component of a module structure *)
@@ -383,9 +397,9 @@ and module_implementation =
   | Struct of module_signature (** interactive body *)
   | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
-and module_body =
-  { mod_mp : module_path; (** absolute path of the module *)
-    mod_expr : module_implementation; (** implementation *)
+and 'a generic_module_body =
+  { mod_mp : ModPath.t; (** absolute path of the module *)
+    mod_expr : 'a; (** implementation *)
     mod_type : module_signature; (** expanded type *)
     (** algebraic type, kept if it's relevant for extraction *)
     mod_type_alg : module_expression option;
@@ -393,13 +407,19 @@ and module_body =
     mod_constraints : Univ.ContextSet.t;
     (** quotiented set of equivalent constants and inductive names *)
     mod_delta : delta_resolver;
-    mod_retroknowledge : action list }
+    mod_retroknowledge : 'a module_retroknowledge; }
+
+and module_body = module_implementation generic_module_body
 
 (** A [module_type_body] is just a [module_body] with no
-    implementation ([mod_expr] always [Abstract]) and also
-    an empty [mod_retroknowledge] *)
+    implementation and also an empty [mod_retroknowledge] *)
+
+and module_type_body = unit generic_module_body
 
-and module_type_body = module_body
+and _ module_retroknowledge =
+| ModBodyRK :
+  action list -> module_implementation module_retroknowledge
+| ModTypeRK : unit module_retroknowledge
 
 (*************************************************************************)
 (** {4 From safe_typing.ml} *)
diff --git a/checker/closure.ml b/checker/closure.ml
index cef1d31a..b9ae4daa 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Util
@@ -49,13 +51,6 @@ let with_stats c =
   end else
     Lazy.force c
 
-type transparent_state = Id.Pred.t * Cpred.t
-let all_opaque = (Id.Pred.empty, Cpred.empty)
-let all_transparent = (Id.Pred.full, Cpred.full)
-
-let is_transparent_variable (ids, _) id = Id.Pred.mem id ids
-let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
-
 module type RedFlagsSig = sig
   type reds
   type red_kind
@@ -63,8 +58,6 @@ module type RedFlagsSig = sig
   val fDELTA : red_kind
   val fIOTA : red_kind
   val fZETA : red_kind
-  val fCONST : constant -> red_kind
-  val fVAR : Id.t -> red_kind
   val no_red : reds
   val red_add : reds -> red_kind -> reds
   val mkflags : red_kind list -> reds
@@ -80,51 +73,33 @@ module RedFlags = (struct
   type reds = {
     r_beta : bool;
     r_delta : bool;
-    r_const : transparent_state;
     r_zeta : bool;
     r_evar : bool;
     r_iota : bool }
 
   type red_kind = BETA | DELTA | IOTA | ZETA
-	      | CONST of constant | VAR of Id.t
+
   let fBETA = BETA
   let fDELTA = DELTA
   let fIOTA = IOTA
   let fZETA = ZETA
-  let fCONST kn  = CONST kn
-  let fVAR id  = VAR id
   let no_red = {
     r_beta = false;
     r_delta = false;
-    r_const = all_opaque;
     r_zeta = false;
     r_evar = false;
     r_iota = false }
 
   let red_add red = function
     | BETA -> { red with r_beta = true }
-    | DELTA -> { red with r_delta = true; r_const = all_transparent }
-    | CONST kn ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = l1, Cpred.add kn l2 }
+    | DELTA -> { red with r_delta = true}
     | IOTA -> { red with r_iota = true }
     | ZETA -> { red with r_zeta = true }
-    | VAR id ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = Id.Pred.add id l1, l2 }
 
   let mkflags = List.fold_left red_add no_red
 
   let red_set red = function
     | BETA -> incr_cnt red.r_beta beta
-    | CONST kn ->
-	let (_,l) = red.r_const in
-	let c = Cpred.mem kn l in
-	incr_cnt c delta
-    | VAR id -> (* En attendant d'avoir des kn pour les Var *)
-	let (l,_) = red.r_const in
-	let c = Id.Pred.mem id l in
-	incr_cnt c delta
     | ZETA -> incr_cnt red.r_zeta zeta
     | IOTA -> incr_cnt red.r_iota iota
     | DELTA -> (* Used for Rel/Var defined in context *)
@@ -160,22 +135,16 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
  * instantiations (cbv or lazy) are.
  *)
 
-type 'a tableKey =
-  | ConstKey of 'a
-  | VarKey of Id.t
-  | RelKey of int
+type table_key = Constant.t puniverses tableKey
+
 
-type table_key = constant puniverses tableKey
+let eq_pconstant_key (c,u) (c',u') =
+  eq_constant_key c c' && Univ.Instance.equal u u'
 
 module KeyHash =
 struct
   type t = table_key
-  let equal k1 k2 = match k1, k2 with
-  | ConstKey (c1,u1), ConstKey (c2,u2) -> Constant.UserOrd.equal c1 c2 
-    && Univ.Instance.equal u1 u2
-  | VarKey id1, VarKey id2 -> Id.equal id1 id2
-  | RelKey i1, RelKey i2 -> Int.equal i1 i2
-  | (ConstKey _ | VarKey _ | RelKey _), _ -> false
+  let equal = Names.eq_table_key eq_pconstant_key
 
   open Hashset.Combine
 
@@ -226,8 +195,6 @@ let defined_rels flags env =
 
 let mind_equiv_infos info = mind_equiv info.i_env
 
-let eq_table_key = KeyHash.equal
-
 let create mk_cl flgs env =
   { i_flags = flgs;
     i_repr = mk_cl;
@@ -276,14 +243,13 @@ and fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of projection * fconstr
+  | FProj of Projection.t * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
-  | FCase of case_info * fconstr * fconstr * fconstr array
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
-  | FLambda of int * (name * constr) list * constr * fconstr subs
-  | FProd of name * fconstr * fconstr
-  | FLetIn of name * fconstr * fconstr * constr * fconstr subs
+  | FLambda of int * (Name.t * constr) list * constr * fconstr subs
+  | FProd of Name.t * fconstr * fconstr
+  | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
   | FEvar of existential_key * fconstr array (* why diff from kernel/closure? *)
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
@@ -306,9 +272,8 @@ let update v1 (no,t) =
 
 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 * projection
+  | Zproj of int * int * Projection.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -328,6 +293,12 @@ let zshift n s =
     | (_,Zshift(k)::s) -> Zshift(n+k)::s
     | _ -> Zshift(n)::s
 
+let rec stack_args_size = function
+  | Zapp v :: s -> Array.length v + stack_args_size s
+  | Zshift(_)::s -> stack_args_size s
+  | Zupdate(_)::s -> stack_args_size s
+  | _ -> 0
+
 (* Lifting. Preserves sharing (useful only for cell with norm=Red).
    lft_fconstr always create a new cell, while lift_fconstr avoids it
    when the lift is 0. *)
@@ -450,13 +421,10 @@ let rec to_constr constr_fun lfts v =
     | FFlex (ConstKey op) -> Const op
     | FInd op -> Ind op
     | FConstruct op -> Construct op
-    | FCase (ci,p,c,ve) ->
-	Case (ci, constr_fun lfts p,
-              constr_fun lfts c,
-	      Array.map (constr_fun lfts) ve)
-    | FCaseT (ci,p,c,ve,e) -> (* TODO: enable sharing, cf FCLOS below ? *)
-        to_constr constr_fun lfts
-	  {norm=Red;term=FCase(ci,mk_clos2 e p,c,mk_clos_vect e ve)}
+    | FCaseT (ci,p,c,ve,e) ->
+       let fp = mk_clos2 e p in
+       let fve = mk_clos_vect e ve in
+       Case (ci, constr_fun lfts fp, constr_fun lfts c, Array.map (constr_fun lfts) fve)
     | FFix ((op,(lna,tys,bds)),e) ->
         let n = Array.length bds in
         let ftys = Array.map (mk_clos e) tys in
@@ -526,9 +494,6 @@ let rec zip m stk =
   match stk with
     | [] -> m
     | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s
-    | Zcase(ci,p,br)::s ->
-        let t = FCase(ci, p, m, br) in
-        zip {norm=neutr m.norm; term=t} s
     | ZcaseT(ci,p,br,e)::s ->
         let t = FCaseT(ci, p, m, br, e) in
         zip {norm=neutr m.norm; term=t} s
@@ -610,7 +575,7 @@ let rec get_args n tys f e stk =
 
 (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
 let rec eta_expand_stack = function
-  | (Zapp _ | Zfix _ | Zcase _ | ZcaseT _ | Zproj _ 
+  | (Zapp _ | Zfix _ | ZcaseT _ | Zproj _
 	| Zshift _ | Zupdate _ as e) :: s ->
       e :: eta_expand_stack s
   | [] ->
@@ -651,22 +616,6 @@ let drop_parameters depth n argstk =
 
 (** Projections and eta expansion *)
 
-let rec get_parameters depth n argstk =
-  match argstk with
-      Zapp args::s ->
-        let q = Array.length args in
-        if n > q then Array.append args (get_parameters depth (n-q) s)
-        else if Int.equal n q then [||]
-        else Array.sub args 0 n
-    | Zshift(k)::s -> 
-      get_parameters (depth-k) n s
-    | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *)
-	if Int.equal n 0 then [||]
-	else raise Not_found (* Trying to eta-expand a partial application..., should do 
-				eta expansion first? *)
-    | _ -> assert false
-	(* strip_update_shift_app only produces Zapp and Zshift items *)
-
 let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.mind_record with
@@ -718,6 +667,9 @@ let contract_fix_vect fix =
   in
   (subs_cons(Array.init nfix make_body, env), thisbody)
 
+let unfold_projection env p =
+  let pb = lookup_projection p env in
+  Zproj (pb.proj_npars, pb.proj_arg, p)
 
 (*********************************************************************)
 (* A machine that inspects the head of a term until it finds an
@@ -730,7 +682,6 @@ let rec knh info m stk =
     | FCLOS(t,e) -> knht info e t (zupdate m stk)
     | FLOCKED -> assert false
     | FApp(a,b) -> knh info a (append_stack b (zupdate m stk))
-    | FCase(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk)
     | FCaseT(ci,p,t,br,env) -> knh info t (ZcaseT(ci,p,br,env)::zupdate m stk)
     | FFix(((ri,n),(_,_,_)),_) ->
         (match get_nth_arg m ri.(n) stk with
@@ -739,10 +690,9 @@ let rec knh info m stk =
     | FCast(t,_,_) -> knh info t stk
 
     | FProj (p,c) ->
-      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))
+      if red_set info.i_flags fDELTA then
+        let s = unfold_projection info.i_env p in
+        knh info c (s :: zupdate m stk)
       else (m,stk)
 
 (* cases where knh stops *)
@@ -774,11 +724,11 @@ let rec knr info m stk =
       (match get_args n tys f e stk with
           Inl e', s -> knit info e' f s
         | Inr lam, s -> (lam,s))
-  | FFlex(ConstKey kn) when red_set info.i_flags (fCONST (fst kn)) ->
+  | FFlex(ConstKey kn) when red_set info.i_flags fDELTA ->
       (match ref_value_cache info (ConstKey kn) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
-  | FFlex(VarKey id) when red_set info.i_flags (fVAR id) ->
+  | FFlex(VarKey id) when red_set info.i_flags fDELTA ->
       (match ref_value_cache info (VarKey id) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
@@ -788,10 +738,6 @@ let rec knr info m stk =
         | None -> (set_norm m; (m,stk)))
   | FConstruct((ind,c),u) when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
-          (depth, args, Zcase(ci,_,br)::s) ->
-            assert (ci.ci_npar>=0);
-            let rargs = drop_parameters depth ci.ci_npar args in
-            kni info br.(c-1) (rargs@s)
        | (depth, args, ZcaseT(ci,_,br,env)::s) ->
             assert (ci.ci_npar>=0);
             let rargs = drop_parameters depth ci.ci_npar args in
@@ -808,7 +754,7 @@ let rec knr info m stk =
        | (_,args,s) -> (m,args@s))
   | FCoFix _ when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
-          (_, args, (((Zcase _|ZcaseT _)::_) as stk')) ->
+          (_, args, (((ZcaseT _|Zproj _)::_) as stk')) ->
             let (fxe,fxbd) = contract_fix_vect m.term in
             knit info fxe fxbd (args@stk')
         | (_,args,s) -> (m,args@s))
@@ -845,6 +791,7 @@ type clos_infos = fconstr infos
 
 let infos_env x = x.i_env
 let infos_flags x = x.i_flags
+let oracle_of_infos x = x.i_env.env_conv_oracle
 
 let create_clos_infos flgs env =
   create (fun _ -> inject) flgs env
diff --git a/checker/closure.mli b/checker/closure.mli
index 8b1f246c..49b07f73 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
@@ -24,14 +26,6 @@ val with_stats: 'a Lazy.t -> 'a
   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
   a LetIn expression is Letin reduction *)
 
-type transparent_state = Id.Pred.t * Cpred.t
-
-val all_opaque      : transparent_state
-val all_transparent : transparent_state
-
-val is_transparent_variable : transparent_state -> variable -> bool
-val is_transparent_constant : transparent_state -> constant -> bool
-
 (* Sets of reduction kinds. *)
 module type RedFlagsSig = sig
   type reds
@@ -42,8 +36,6 @@ module type RedFlagsSig = sig
   val fDELTA : red_kind
   val fIOTA : red_kind
   val fZETA : red_kind
-  val fCONST : constant -> red_kind
-  val fVAR : Id.t -> red_kind
 
   (* No reduction at all *)
   val no_red : reds
@@ -66,12 +58,8 @@ val betaiotazeta       : reds
 val betadeltaiotanolet : reds
 
 (***********************************************************************)
-type 'a tableKey =
-  | ConstKey of 'a
-  | VarKey of Id.t
-  | RelKey of int
 
-type table_key = constant puniverses tableKey
+type table_key = Constant.t puniverses tableKey
 
 type 'a infos
 val ref_value_cache: 'a infos -> table_key -> 'a option
@@ -95,14 +83,13 @@ type fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of projection * fconstr
+  | FProj of Projection.t * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
-  | FCase of case_info * fconstr * fconstr * fconstr array
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
-  | FLambda of int * (name * constr) list * constr * fconstr subs
-  | FProd of name * fconstr * fconstr
-  | FLetIn of name * fconstr * fconstr * constr * fconstr subs
+  | FLambda of int * (Name.t * constr) list * constr * fconstr subs
+  | FProd of Name.t * fconstr * fconstr
+  | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
   | FEvar of existential_key * fconstr array
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
@@ -115,9 +102,8 @@ type fterm =
 
 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 * projection
+  | Zproj of int * int * Projection.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -125,11 +111,16 @@ type stack_member =
 and stack = stack_member list
 
 val append_stack : fconstr array -> stack -> stack
+
+val stack_args_size : stack -> int
+    
 val eta_expand_stack : stack -> stack
  
 val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> 
    (fconstr * stack) -> stack * stack
 
+val unfold_projection : env -> Projection.t -> stack_member
+
 (* To lazy reduce a constr, create a [clos_infos] with
    [create_clos_infos], inject the term to reduce with [inject]; then use
    a reduction function *)
@@ -139,13 +130,15 @@ val inject : constr -> fconstr
 val fterm_of : fconstr -> fterm
 val term_of_fconstr : fconstr -> constr
 val destFLambda :
-  (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr
+  (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr
 
 (* Global and local constant cache *)
 type clos_infos
 val create_clos_infos : reds -> env -> clos_infos
 val infos_env : clos_infos -> env
 val infos_flags : clos_infos -> reds
+val oracle_of_infos : clos_infos -> oracle
+
 
 (* Reduction function *)
 
@@ -165,7 +158,6 @@ val unfold_reference : clos_infos -> table_key -> fconstr option
 (* [mind_equiv] checks whether two inductive types are intentionally equal *)
 val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool
 
-val eq_table_key : table_key -> table_key -> bool
 (************************************************************************)
 (*i This is for lazy debug *)
 
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 1fe02c8b..d2c3f203 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -6,6 +6,7 @@ open Term
 (** Substitutions, code imported from kernel/mod_subst *)
 
 module Deltamap = struct
+  [@@@ocaml.warning "-32-34"]
   type t = delta_resolver
   let empty = MPmap.empty, KNmap.empty
   let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km
@@ -25,6 +26,7 @@ end
 let empty_delta_resolver = Deltamap.empty
 
 module Umap = struct
+  [@@@ocaml.warning "-32-34"]
   type 'a t = 'a umap_t
   let empty = MPmap.empty, MBImap.empty
   let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2
@@ -194,7 +196,7 @@ let subst_con0 sub con u =
   let dup con = con, Const (con, u) in
   let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
   match constant_of_delta_with_inline resolve con' with
-    | Some t -> con', t
+    | Some t -> con', subst_instance_constr u t
     | None ->
       let con'' = match side with
 	| User -> constant_of_delta resolve con'
@@ -461,13 +463,6 @@ let is_opaque cb = match cb.const_body with
 
 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
-  if copt == copt' && t == t' then x else (id,copt',t')
-
-let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
-
 let subst_recarg sub r = match r with
   | Norec  -> r
   | (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in
@@ -489,8 +484,8 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
 
 let eq_recarg r1 r2 = match r1, r2 with
   | Norec, Norec -> true
-  | Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
-  | Imbr i1, Imbr i2 -> Names.eq_ind i1 i2
+  | Mrec i1, Mrec i2 -> Names.eq_ind_chk i1 i2
+  | Imbr i1, Imbr i2 -> Names.eq_ind_chk i1 i2
   | _ -> false
 
 let eq_wf_paths = Rtree.equal eq_recarg
@@ -515,27 +510,22 @@ let subst_decl_arity f g sub ar =
       if x' == x then ar
       else TemplateArity x'
 
-let map_decl_arity f g = function
-  | RegularArity a -> RegularArity (f a)
-  | TemplateArity a -> TemplateArity (g a)
-
 let subst_rel_declaration sub =
   Term.map_rel_decl (subst_mps sub)
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
-let subst_template_cst_arity sub (ctx,s as arity) =
-  let ctx' = subst_rel_context sub ctx in
-    if ctx==ctx' then arity else (ctx',s)
-
-let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s
+let constant_is_polymorphic cb =
+  match cb.const_universes with
+  | Monomorphic_const _ -> false
+  | Polymorphic_const _ -> true
 
 (* TODO: should be changed to non-coping after Term.subst_mps *)
 (* NB: we leave bytecode and native code fields untouched *)
 let subst_const_body sub cb =
  { cb with
     const_body = subst_constant_def sub cb.const_body;
-    const_type = subst_arity sub cb.const_type }
+    const_type = subst_mps sub cb.const_type }
 
 
 let subst_regular_ind_arity sub s =
@@ -583,34 +573,36 @@ let implem_map fs fa = function
   | Algebraic a -> Algebraic (fa a)
   | impl -> impl
 
-let subst_with_body sub = function
-  | WithMod(id,mp) -> WithMod(id,subst_mp sub mp)
-  | WithDef(id,(c,ctx)) -> WithDef(id,(subst_mps sub c,ctx))
-
 let rec subst_expr sub = function
   | MEident mp -> MEident (subst_mp sub mp)
   | MEapply (me1,mp2)-> MEapply (subst_expr sub me1, subst_mp sub mp2)
-  | MEwith (me,wd)-> MEwith (subst_expr sub me, subst_with_body sub wd)
+  | MEwith (me,wd)-> MEwith (subst_expr sub me, wd)
 
 let rec subst_expression sub me =
-  functor_map (subst_module sub) (subst_expr sub) me
+  functor_map (subst_module_type sub) (subst_expr sub) me
 
 and subst_signature sub sign =
-  functor_map (subst_module sub) (subst_structure sub) sign
+  functor_map (subst_module_type sub) (subst_structure sub) sign
 
 and subst_structure sub struc =
   let subst_body = function
     | SFBconst cb -> SFBconst (subst_const_body sub cb)
     | SFBmind mib -> SFBmind (subst_mind sub mib)
     | SFBmodule mb -> SFBmodule (subst_module sub mb)
-    | SFBmodtype mtb -> SFBmodtype (subst_module sub mtb)
+    | SFBmodtype mtb -> SFBmodtype (subst_module_type sub mtb)
   in
   List.map (fun (l,b) -> (l,subst_body b)) struc
 
-and subst_module sub mb =
+and subst_body : 'a. (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body =
+  fun subst_impl sub mb ->
   { mb with
     mod_mp = subst_mp sub mb.mod_mp;
-    mod_expr =
-      implem_map (subst_signature sub) (subst_expression sub) mb.mod_expr;
+    mod_expr = subst_impl sub mb.mod_expr;
     mod_type = subst_signature sub mb.mod_type;
     mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg }
+
+and subst_module sub mb =
+  subst_body (fun sub e -> implem_map (subst_signature sub) (subst_expression sub) e) sub mb
+
+and subst_module_type sub mb =
+  subst_body (fun _ () -> ()) sub mb
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 456df836..7458b3e0 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -14,6 +14,7 @@ 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
+val constant_is_polymorphic : constant_body -> bool
 
 (* Mutual inductives *)
 
@@ -33,12 +34,12 @@ val empty_delta_resolver : delta_resolver
 type 'a subst_fun = substitution -> 'a -> 'a
 
 val empty_subst : substitution
-val add_mbid : MBId.t -> module_path -> substitution -> substitution
-val add_mp   : module_path -> module_path -> substitution -> substitution
-val map_mbid : MBId.t -> module_path -> substitution
-val map_mp   : module_path -> module_path -> substitution
-val mp_in_delta : module_path -> delta_resolver -> bool
-val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
+val add_mbid : MBId.t -> ModPath.t -> substitution -> substitution
+val add_mp   : ModPath.t -> ModPath.t -> substitution -> substitution
+val map_mbid : MBId.t -> ModPath.t -> substitution
+val map_mp   : ModPath.t -> ModPath.t -> substitution
+val mp_in_delta : ModPath.t -> delta_resolver -> bool
+val mind_of_delta : delta_resolver -> MutInd.t -> MutInd.t
 
 val subst_const_body : constant_body subst_fun
 val subst_mind : mutual_inductive_body subst_fun
diff --git a/checker/environ.ml b/checker/environ.ml
index 7b59c6b9..bbd043c8 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -8,7 +8,7 @@ open Declarations
 type globals = {
   env_constants : constant_body Cmap_env.t;
   env_inductives : mutual_inductive_body Mindmap_env.t;
-  env_inductives_eq : kernel_name  KNmap.t;
+  env_inductives_eq : KerName.t KNmap.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
 
@@ -21,7 +21,15 @@ type env = {
     env_globals       : globals;
     env_rel_context   : rel_context;
     env_stratification : stratification;
-    env_imports : Cic.vodigest MPmap.t }
+    env_imports : Cic.vodigest MPmap.t;
+    env_conv_oracle : oracle; }
+
+let empty_oracle = {
+  var_opacity = Id.Map.empty;
+  cst_opacity = Cmap.empty;
+  var_trstate = Id.Pred.empty;
+  cst_trstate = Cpred.empty;
+}
 
 let empty_env = {
   env_globals =
@@ -34,7 +42,8 @@ let empty_env = {
   env_stratification =
   { env_universes = Univ.initial_universes;
     env_engagement = PredicativeSet };
-  env_imports = MPmap.empty }
+  env_imports = MPmap.empty;
+  env_conv_oracle = empty_oracle }
 
 let engagement env = env.env_stratification.env_engagement
 let universes env = env.env_stratification.env_universes
@@ -45,12 +54,14 @@ let set_engagement (impr_set as c) env =
     env.env_stratification.env_engagement in
   begin
     match impr_set,expected_impr_set with
-    | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement"
+    | PredicativeSet, ImpredicativeSet -> user_err Pp.(str "Incompatible engagement")
     | _ -> ()
   end;
   { env with env_stratification =
       { env.env_stratification with env_engagement = c } }
 
+let set_oracle env oracle = { env with env_conv_oracle = oracle }
+
 (* Digests *)
 
 let add_digest env dp digest =
@@ -106,7 +117,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")
+    Printf.ksprintf anomaly ("Constant %s is already defined.")
       (Constant.to_string kn);
   let new_constants =
     Cmap_env.add kn cs env.env_globals.env_constants in
@@ -120,35 +131,33 @@ type const_evaluation_result = NoBody | Opaque
 (* Constant types *)
 
 let constraints_of cb u =
-  let univs = cb.const_universes in
-    Univ.subst_instance_constraints u (Univ.UContext.constraints univs)
-
-let map_regular_arity f = function
-  | RegularArity a as ar -> 
-    let a' = f a in 
-      if a' == a then ar else RegularArity a'
-  | TemplateArity _ -> assert false
+  match cb.const_universes with
+  | Monomorphic_const _ -> Univ.Constraint.empty
+  | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
 
 (* constant_type gives the type of a constant *)
 let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
-    if cb.const_polymorphic then
-      let csts = constraints_of cb u in
-	(map_regular_arity (subst_instance_constr u) cb.const_type, csts)
-    else cb.const_type, Univ.Constraint.empty
+  match cb.const_universes with
+  | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
+  | Polymorphic_const ctx -> 
+    let csts = constraints_of cb u in
+    (subst_instance_constr u cb.const_type, csts)
 
 exception NotEvaluableConst of const_evaluation_result
 
 let constant_value env (kn,u) =
   let cb = lookup_constant kn env in
-    match cb.const_body with
-    | Def l_body -> 
-      let b = force_constr l_body in
-	if cb.const_polymorphic then
-	  subst_instance_constr u (force_constr l_body)
-	else b
-    | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
-    | Undef _ -> raise (NotEvaluableConst NoBody)
+  match cb.const_body with
+  | Def l_body ->
+    let b = force_constr l_body in
+    begin
+      match cb.const_universes with
+      | Monomorphic_const _ -> b
+      | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body)
+    end
+  | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
+  | Undef _ -> raise (NotEvaluableConst NoBody)
 
 (* A global const is evaluable if it is defined and not opaque *)
 let evaluable_constant cst env =
@@ -161,7 +170,7 @@ let is_projection cst env =
 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")
+  | None -> anomaly ("lookup_projection: constant is not a projection.")
 
 (* Mutual Inductives *)
 let scrape_mind env kn=
@@ -182,7 +191,7 @@ 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")
+    Printf.ksprintf anomaly ("Inductive %s is already defined.")
       (MutInd.to_string kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
   let kn1,kn2 =  MutInd.user kn, MutInd.canonical kn in
@@ -201,7 +210,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")
+    Printf.ksprintf anomaly ("Module type %s is already defined.")
       (ModPath.to_string ln);
   let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
   let new_globals =
@@ -211,7 +220,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")
+    Printf.ksprintf anomaly ("Module %s is already defined.")
       (ModPath.to_string mp);
   let new_mods = MPmap.add mp mb env.env_globals.env_modules in
   let new_globals =
@@ -221,7 +230,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")
+    Printf.ksprintf anomaly ("Module %s is unknown.")
       (ModPath.to_string mp);
   let new_mods = MPmap.remove mp env.env_globals.env_modules in
   let new_globals =
diff --git a/checker/environ.mli b/checker/environ.mli
index 87f143d1..81da8387 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -6,7 +6,7 @@ open Cic
 type globals = {
   env_constants : constant_body Cmap_env.t;
   env_inductives : mutual_inductive_body Mindmap_env.t;
-  env_inductives_eq : kernel_name KNmap.t;
+  env_inductives_eq : KerName.t KNmap.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
 type stratification = {
@@ -18,6 +18,7 @@ type env = {
   env_rel_context : rel_context;
   env_stratification : stratification;
   env_imports : Cic.vodigest MPmap.t;
+  env_conv_oracle : Cic.oracle;
 }
 val empty_env : env
 
@@ -25,6 +26,10 @@ val empty_env : env
 val engagement : env -> Cic.engagement
 val set_engagement : Cic.engagement -> env -> env
 
+(** Oracle *)
+
+val set_oracle : env -> Cic.oracle -> env
+
 (* Digests *)
 val add_digest : env -> DirPath.t -> Cic.vodigest -> env
 val lookup_digest : env -> DirPath.t -> Cic.vodigest
@@ -34,7 +39,7 @@ val rel_context : env -> rel_context
 val lookup_rel : int -> env -> rel_declaration
 val push_rel : rel_declaration -> env -> env
 val push_rel_context : rel_context -> env -> env
-val push_rec_types : name array * constr array * 'a -> env -> env
+val push_rec_types : Name.t array * constr array * 'a -> env -> env
 
 (* Universes *)
 val universes : env -> Univ.universes
@@ -44,31 +49,31 @@ val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
 val check_constraints : Univ.constraints -> env -> bool
 
 (* Constants *)
-val lookup_constant : constant -> env -> Cic.constant_body
-val add_constant : constant -> Cic.constant_body -> env -> env
-val constant_type : env -> constant puniverses -> constant_type Univ.constrained
+val lookup_constant : Constant.t -> env -> Cic.constant_body
+val add_constant : Constant.t -> Cic.constant_body -> env -> env
+val constant_type : env -> Constant.t puniverses -> constr Univ.constrained
 type const_evaluation_result = NoBody | Opaque
 exception NotEvaluableConst of const_evaluation_result
-val constant_value : env -> constant puniverses -> constr
-val evaluable_constant : constant -> env -> bool
+val constant_value : env -> Constant.t puniverses -> constr
+val evaluable_constant : Constant.t -> env -> bool
 
-val is_projection : constant -> env -> bool
-val lookup_projection : projection -> env -> projection_body
+val is_projection : Constant.t -> env -> bool
+val lookup_projection : Projection.t -> env -> projection_body
 
 (* Inductives *)
 val mind_equiv : env -> inductive -> inductive -> bool
 
 val lookup_mind :
-  mutual_inductive -> env -> Cic.mutual_inductive_body
+  MutInd.t -> env -> Cic.mutual_inductive_body
 
 val add_mind :
-  mutual_inductive -> Cic.mutual_inductive_body -> env -> env
+  MutInd.t -> Cic.mutual_inductive_body -> env -> env
 
 (* Modules *)
 val add_modtype :
-  module_path -> Cic.module_type_body -> env -> env
+  ModPath.t -> Cic.module_type_body -> env -> env
 val shallow_add_module :
-  module_path -> Cic.module_body -> env -> env
-val shallow_remove_module : module_path -> env -> env
-val lookup_module : module_path -> env -> Cic.module_body
-val lookup_modtype : module_path -> env -> Cic.module_type_body
+  ModPath.t -> Cic.module_body -> env -> env
+val shallow_remove_module : ModPath.t -> env -> env
+val lookup_module : ModPath.t -> env -> Cic.module_body
+val lookup_modtype : ModPath.t -> env -> Cic.module_type_body
diff --git a/checker/include b/checker/include
index 6bea3c91..da034635 100644
--- a/checker/include
+++ b/checker/include
@@ -13,7 +13,6 @@
 #directory "kernel";;
 #directory "checker";;
 #directory "+threads";;
-#directory "+camlp4";;
 #directory "+camlp5";;
 
 #load "unix.cma";;
@@ -116,7 +115,7 @@ let prsub s =
 #install_printer prsub;;*)
 
 Checker.init_with_argv [|"";"-coqlib";"."|];;
-Flags.make_silent false;;
+Flags.quiet := false;;
 Flags.debug := true;;
 Sys.catch_break true;;
 
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 27f79e79..916934a8 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open CErrors
@@ -100,7 +102,7 @@ let rec sorts_of_constr_args env t =
         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")
+    | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor.")
 
 
 (* Prop and Set are small *)
@@ -302,11 +304,11 @@ let failwith_non_pos n ntypes c =
 
 let failwith_non_pos_vect n ntypes v =
   Array.iter (failwith_non_pos n ntypes) v;
-  anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur")
+  anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur.")
 
 let failwith_non_pos_list n ntypes l =
   List.iter (failwith_non_pos n ntypes) l;
-  anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur")
+  anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.")
 
 (* Conclusion of constructors: check the inductive type is called with
    the expected parameters *)
@@ -502,10 +504,19 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
       indlc
   in mk_paths (Mrec ind) irecargs
 
+let prrecarg = function
+  | Norec -> str "Norec"
+  | Mrec (mind,i) ->
+     str "Mrec[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]"
+  | Imbr (mind,i) ->
+     str "Imbr[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]"
+
 let check_subtree t1 t2 =
   let cmp_labels l1 l2 = l1 == Norec || eq_recarg l1 l2 in
   if not (Rtree.equiv eq_recarg cmp_labels t1 t2)
-  then failwith "bad recursive trees"
+  then user_err Pp.(str "Bad recursive tree: found " ++ fnl ()
+    ++ Rtree.pp_tree prrecarg t1 ++ fnl () ++ str " when expected " ++ fnl ()
+    ++ Rtree.pp_tree prrecarg t2)
 (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*)
 
 let check_positivity env_ar mind params nrecp inds =
@@ -524,29 +535,104 @@ let check_positivity env_ar mind params nrecp inds =
   let wfp = Rtree.mk_rec irecargs in
   Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp
 
+(* Check arities and constructors *)
+let check_subtyping_arity_constructor env (subst : Univ.Instance.t) (arcn : constr) numparams is_arity =
+  let numchecked = ref 0 in
+  let basic_check ev tp =
+    if !numchecked < numparams then () else conv_leq ev tp (Term.subst_instance_constr subst tp);
+    numchecked := !numchecked + 1
+  in
+  let check_typ typ typ_env =
+    match typ with
+    | LocalAssum (_, typ') ->
+      begin
+       try
+          basic_check typ_env typ'; Environ.push_rel typ typ_env
+        with NotConvertible -> 
+          anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation")
+      end
+    | _ -> anomaly (Pp.str "")
+  in
+  let typs, codom = dest_prod env arcn in
+  let last_env = fold_rel_context_outside check_typ typs ~init:env in
+  if not is_arity then basic_check last_env codom else ()
+
+(* Check that the subtyping information inferred for inductive types in the block is correct. *)
+(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
+let check_subtyping cumi paramsctxt env inds =
+  let open Univ in
+  let numparams = rel_context_nhyps paramsctxt in
+  (** In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available.
+      We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n]
+      and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together
+      with the cumulativity constraints [ cumul_cst ]. *)
+  let uctx = ACumulativityInfo.univ_context cumi in
+  let len = AUContext.size uctx in
+  let inst = Instance.of_array @@ Array.init len (fun i -> Level.var (i + len)) in
+
+  let other_context = ACumulativityInfo.univ_context cumi in
+  let uctx_other = UContext.make (inst, AUContext.instantiate inst other_context) in
+  let cumul_cst =
+    Array.fold_left_i (fun i csts var ->
+        match var with
+        | Variance.Irrelevant -> csts
+        | Variance.Covariant -> Constraint.add (Level.var i,Le,Level.var (i+len)) csts
+        | Variance.Invariant -> Constraint.add (Level.var i,Eq,Level.var (i+len)) csts)
+      Constraint.empty (ACumulativityInfo.variance cumi)
+  in
+  let env = Environ.push_context uctx_other env in
+  let env = Environ.add_constraints cumul_cst env in
+
+  (* process individual inductive types: *)
+  Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
+      match arity with
+      | RegularArity { mind_user_arity = full_arity} ->
+        check_subtyping_arity_constructor env inst full_arity numparams true;
+        Array.iter (fun cnt -> check_subtyping_arity_constructor env inst cnt numparams false) lc
+      | TemplateArity _ -> ()
+    ) inds
+    
 (************************************************************************)
 (************************************************************************)
 
 let check_inductive env kn mib =
   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
+  let env0 =
+    match mib.mind_universes with
+    | Monomorphic_ind _ -> env
+    | Polymorphic_ind auctx ->
+      let uctx = Univ.AUContext.repr auctx in
+      Environ.push_context uctx env
+    | Cumulative_ind cumi -> 
+      let uctx = Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in
+      Environ.push_context uctx env
+  in
+  (** Locally set the oracle for further typechecking *)
+  let env0 = Environ.set_oracle env0 mib.mind_typing_flags.conv_oracle in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
   (* check mind_finite : always OK *)
   (* check mind_ntypes *)
   if Array.length mib.mind_packets <> mib.mind_ntypes then
-    error "not the right number of packets";
+    user_err Pp.(str "not the right number of packets");
   (* check mind_params_ctxt *)
   let params = mib.mind_params_ctxt in
-  let _ = check_ctxt env params in
+  let _ = check_ctxt env0 params in
   (* check mind_nparams *)
   if rel_context_nhyps params <> mib.mind_nparams then
-    error "number the right number of parameters";
+    user_err Pp.(str "number the right number of parameters");
   (* mind_packets *)
   (*  - check arities *)
-  let env_ar = typecheck_arity env params mib.mind_packets in
+  let env_ar = typecheck_arity env0 params mib.mind_packets in
   (*  - check constructor types *)
   Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
+  (* check the inferred subtyping relation *)
+  let () = 
+    match mib.mind_universes with
+    | Monomorphic_ind _ | Polymorphic_ind _ -> ()
+    | Cumulative_ind acumi ->
+      check_subtyping acumi params env_ar mib.mind_packets
+  in
   (* check mind_nparams_rec: positivity condition *)
   check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
   (* check mind_equiv... *)
diff --git a/checker/indtypes.mli b/checker/indtypes.mli
index 071eecbb..baaa66a6 100644
--- a/checker/indtypes.mli
+++ b/checker/indtypes.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
@@ -12,8 +14,8 @@ open Cic
 open Environ
 (*i*)
 
-val prkn : kernel_name -> Pp.std_ppcmds
-val prcon : constant -> Pp.std_ppcmds
+val prkn : KerName.t -> Pp.t
+val prcon : Constant.t -> Pp.t
 
 (*s The different kinds of errors that may result of a malformed inductive
   definition. *)
@@ -34,4 +36,4 @@ exception InductiveError of inductive_error
 
 (*s The following function does checks on inductive declarations. *)
 
-val check_inductive : env -> mutual_inductive -> mutual_inductive_body -> env
+val check_inductive : env -> MutInd.t -> mutual_inductive_body -> env
diff --git a/checker/inductive.ml b/checker/inductive.ml
index c4ffc141..e1c6b135 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open CErrors
@@ -27,7 +29,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body
 let lookup_mind_specif env (kn,tyi) =
   let mib = lookup_mind kn env in
   if tyi >= Array.length mib.mind_packets then
-    error "Inductive.lookup_mind_specif: invalid inductive index";
+    user_err Pp.(str "Inductive.lookup_mind_specif: invalid inductive index");
   (mib, mib.mind_packets.(tyi))
 
 let find_rectype env c =
@@ -54,10 +56,17 @@ let inductive_params (mib,_) = mib.mind_nparams
 
 (** Polymorphic inductives *)
 
-let inductive_instance mib =
-  if mib.mind_polymorphic then
-    UContext.instance mib.mind_universes
-  else Instance.empty
+let inductive_is_polymorphic mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> false
+  | Polymorphic_ind ctx -> true
+  | Cumulative_ind cumi -> true
+
+let inductive_is_cumulative mib =
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> false
+  | Polymorphic_ind ctx -> false
+  | Cumulative_ind cumi -> true
 
 (************************************************************************)
 
@@ -75,7 +84,7 @@ let constructor_instantiate mind u mib c =
 
 let instantiate_params full t u args sign =
   let fail () =
-    anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
+    anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in
   let (rem_args, subs, ty) =
     fold_rel_context
       (fun decl (largs,subs,ty) ->
@@ -93,7 +102,7 @@ let instantiate_params full t u args sign =
 
 let full_inductive_instantiate mib u params sign =
   let dummy = Prop Null in
-  let t = mkArity (subst_instance_context u sign,dummy) in
+  let t = mkArity (Term.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) t =
@@ -149,7 +158,7 @@ let remember_subst u subst =
 
 (* Bind expected levels of parameters to actual levels *)
 (* Propagate the new levels in the signature *)
-let rec make_subst env =
+let make_subst env =
   let rec make subst = function
     | LocalDef _ :: sign, exp, args ->
         make subst (sign, exp, args)
@@ -199,7 +208,7 @@ let instantiate_universes env ctx ar argsorts =
 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
+    if not (inductive_is_polymorphic mib) then a.mind_user_arity
     else subst_instance_constr u a.mind_user_arity
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
@@ -232,7 +241,7 @@ let type_of_constructor_subst cstr u (mib,mip) =
   let specif = mip.mind_user_lc in
   let i = index_of_constructor cstr in
   let nconstr = Array.length mip.mind_consnames in
-  if i > nconstr then error "Not enough constructors in the type.";
+  if i > nconstr then user_err Pp.(str "Not enough constructors in the type.");
     constructor_instantiate (fst ind) u mib specif.(i-1)
 
 let type_of_constructor_gen (cstr,u) (mib,mip as mspec) =
@@ -374,7 +383,7 @@ let type_case_branches env (pind,largs) (p,pj) c =
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
-    not (eq_ind indsp ci.ci_ind) ||
+    not (eq_ind_chk indsp ci.ci_ind) ||
     (mib.mind_nparams <> ci.ci_npar) ||
     (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) ||
     (mip.mind_consnrealargs <> ci.ci_cstr_nargs)
@@ -428,27 +437,14 @@ type subterm_spec =
   | Dead_code
   | Not_subterm
 
-let eq_recarg r1 r2 = match r1, r2 with
-| Norec, Norec -> true
-| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
-| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2
-| _ -> false
-
 let eq_wf_paths = Rtree.equal eq_recarg
 
-let pp_recarg = function
-  | Norec -> Pp.str "Norec"
-  | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i))
-  | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i))
-
-let pp_wf_paths = Rtree.pp_tree pp_recarg
-
 let inter_recarg r1 r2 = match r1, r2 with
 | Norec, Norec -> Some r1
 | Mrec i1, Mrec i2
 | Imbr i1, Imbr i2
-| Mrec i1, Imbr i2 -> if Names.eq_ind i1 i2 then Some r1 else None
-| Imbr i1, Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None
+| Mrec i1, Imbr i2 -> if Names.eq_ind_chk i1 i2 then Some r1 else None
+| Imbr i1, Mrec i2 -> if Names.eq_ind_chk i1 i2 then Some r2 else None
 | _ -> None
 
 let inter_wf_paths = Rtree.inter eq_recarg inter_recarg Norec
@@ -544,7 +540,7 @@ let lookup_subterms env ind =
 
 let match_inductive ind ra =
   match ra with
-    | (Mrec i | Imbr i) -> eq_ind ind i
+    | (Mrec i | Imbr i) -> eq_ind_chk ind i
     | Norec -> false
 
 (* In {match c as z in ci y_s return P with |C_i x_s => t end}
@@ -645,7 +641,7 @@ let get_recargs_approx env tree ind args =
        (* When the inferred tree allows it, we consider that we have a potential
        nested inductive type *)
        begin match dest_recarg tree with
-	     | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' ->
+             | Imbr kn' | Mrec kn' when eq_ind_chk (fst ind_kn) kn' ->
 			   build_recargs_nested ienv tree (ind_kn, largs)
 	     | _ -> mk_norec
        end
@@ -993,7 +989,7 @@ let check_one_fix renv recpos trees def =
             List.iter (check_rec_call renv []) l;
             check_rec_call renv [] c
 
-        | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
+        | Var _ -> anomaly (Pp.str "Section variable in Coqchk!")
 
 	| Sort _ -> assert (l = [])
 
@@ -1011,7 +1007,7 @@ let check_one_fix renv recpos trees def =
 	    check_rec_call renv [] a;
             let renv' = push_var_renv renv (x,a) in
 	      check_nested_fix_body renv' (decr-1) recArgsDecrArg b
-	| _ -> anomaly (Pp.str "Not enough abstractions in fix body")
+	| _ -> anomaly (Pp.str "Not enough abstractions in fix body.")
 	    
   in
   check_rec_call renv [] def
@@ -1025,7 +1021,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     || Array.length names <> nbfix
     || bodynum < 0
     || bodynum >= nbfix
-  then anomaly (Pp.str "Ill-formed fix term");
+  then anomaly (Pp.str "Ill-formed fix term.");
   let fixenv = push_rec_types recdef env in
   let raise_err env i err =
     error_ill_formed_rec_body env err names i in
@@ -1046,7 +1042,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
 		    raise_err env i (RecursionNotOnInductiveType a) in
                 (mind, (env', b))
 	      else check_occur env' (n+1) b
-            else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call")
+            else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.")
         | _ -> raise_err env i NotEnoughAbstractionInFixBody in
     check_occur fixenv 1 def in
   (* Do it on every fixpoint *)
@@ -1070,8 +1066,8 @@ let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) =
   done
 
 (*
-let cfkey = Profile.declare_profile "check_fix";;
-let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
+let cfkey = CProfile.declare_profile "check_fix";;
+let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;;
 *)
 
 (************************************************************************)
@@ -1080,7 +1076,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
 exception CoFixGuardError of env * guard_error
 
 let anomaly_ill_typed () =
-  anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor")
+  anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor.")
 
 let rec codomain_is_coind env c =
   let b = whd_all env c in
diff --git a/checker/inductive.mli b/checker/inductive.mli
index ed3a7b53..0ca0d14a 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
@@ -22,14 +24,16 @@ type mind_specif = mutual_inductive_body * one_inductive_body
     Raises [Not_found] if the inductive type is not found. *)
 val lookup_mind_specif : env -> inductive -> mind_specif
 
-val inductive_instance : mutual_inductive_body -> Univ.universe_instance
+val inductive_is_polymorphic : mutual_inductive_body -> bool
+
+val inductive_is_cumulative : mutual_inductive_body -> bool
 
 val type_of_inductive : env -> mind_specif puniverses -> constr
 
 (* Return type as quoted by the user *)
 val type_of_constructor : pconstructor -> mind_specif -> constr
 
-val arities_of_specif : mutual_inductive puniverses -> mind_specif -> constr array
+val arities_of_specif : MutInd.t puniverses -> mind_specif -> constr array
 
 (* [type_case_branches env (I,args) (p:A) c] computes useful types
    about the following Cases expression:
diff --git a/checker/main.mli b/checker/main.mli
new file mode 100644
index 00000000..9db9ecd1
--- /dev/null
+++ b/checker/main.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+   that does not have a corresponding .mli file *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 7f93e156..3ef2b340 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -1,9 +1,7 @@
-
 open Pp
 open Util
 open Names
 open Cic
-open Term
 open Reduction
 open Typeops
 open Indtypes
@@ -14,51 +12,39 @@ open Environ
 
 (** {6 Checking constants } *)
 
-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 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
-        mkArity (ctxt,Prop Null), ctx
-    | _ -> ar, Univ.ContextSet.empty
-
 let check_constant_declaration env kn cb =
-  Flags.if_verbose Feedback.msg_notice (str "  checking cst: " ++ prcon kn);
+  Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
+  (** Locally set the oracle for further typechecking *)
+  let oracle = env.env_conv_oracle in
+  let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in
+  (** [env'] contains De Bruijn universe variables *)
   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 = push_context_set cu env' in
-        let _ = infer_type envty ty' in envty, ty
-    | TemplateArity(ctxt,par) ->
-        let _ = check_ctxt env' ctxt in
-        check_polymorphic_arity env' ctxt par;
-	env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt 
+    match cb.const_universes with
+    | Monomorphic_const ctx -> push_context_set ~strict:true ctx env
+    | Polymorphic_const auctx ->
+      let ctx = Univ.AUContext.repr auctx in
+      push_context ~strict:false ctx env
   in
+  let ty = cb.const_type in
+  let () = ignore(infer_type env' ty) in
   let () = 
     match body_of_constant cb with
     | Some bd ->
       (match cb.const_proj with 
-      | None -> let j = infer envty bd in
-		  conv_leq envty j ty
+      | None -> let j = infer env' bd in
+                  conv_leq env' j ty
       | Some pb -> 
 	let env' = add_constant kn cb env' in
 	let j = infer env' bd in
-	  conv_leq envty j ty)
+          conv_leq env' j ty)
     | None -> ()
   in
-  if cb.const_polymorphic then add_constant kn cb env
-  else add_constant kn cb env'
+  let env =
+    if constant_is_polymorphic cb then add_constant kn cb env
+    else add_constant kn cb env'
+  in
+  (** Reset the value of the oracle *)
+  Environ.set_oracle env oracle
 
 (** {6 Checking modules } *)
 
@@ -74,12 +60,12 @@ let lookup_module mp env =
 
 let mk_mtb mp sign delta =
   { mod_mp = mp;
-    mod_expr = Abstract;
+    mod_expr = ();
     mod_type = sign;
     mod_type_alg = None;
     mod_constraints = Univ.ContextSet.empty;
     mod_delta = delta;
-    mod_retroknowledge = []; }
+    mod_retroknowledge = ModTypeRK; }
 
 let rec check_module env mp mb =
   let (_:module_signature) =
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index 5c7b392f..c9e7f9a1 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val check_module : Environ.env -> Names.module_path -> Cic.module_body -> unit
+val check_module : Environ.env -> Names.ModPath.t -> Cic.module_body -> unit
diff --git a/checker/modops.ml b/checker/modops.ml
index b720fb62..c7ad0977 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
@@ -16,29 +18,29 @@ open Declarations
 (*i*)
 
 let error_not_a_constant l =
-  error ("\""^(Label.to_string l)^"\" is not a constant")
+  user_err Pp.(str ("\""^(Label.to_string l)^"\" is not a constant"))
 
-let error_not_a_functor () = error "Application of not a functor"
+let error_not_a_functor () = user_err Pp.(str "Application of not a functor")
 
-let error_incompatible_modtypes _ _ = error "Incompatible module types"
+let error_incompatible_modtypes _ _ = user_err Pp.(str "Incompatible module types")
 
 let error_not_match l _ =
-  error ("Signature components for label "^Label.to_string l^" do not match")
+  user_err Pp.(str ("Signature components for label "^Label.to_string l^" do not match"))
 
-let error_no_such_label l = error ("No such label "^Label.to_string l)
+let error_no_such_label l = user_err Pp.(str ("No such label "^Label.to_string l))
 
 let error_no_such_label_sub l l1 =
   let l1 = ModPath.to_string l1 in
-  error ("The field "^
-         Label.to_string l^" is missing in "^l1^".")
+  user_err Pp.(str ("The field "^
+         Label.to_string l^" is missing in "^l1^"."))
 
-let error_not_a_module_loc loc s =
-  user_err_loc (loc,"",str ("\""^Label.to_string s^"\" is not a module"))
+let error_not_a_module_loc ?loc s =
+  user_err ?loc  (str ("\""^Label.to_string s^"\" is not a module"))
 
-let error_not_a_module s = error_not_a_module_loc Loc.ghost s
+let error_not_a_module s = error_not_a_module_loc s
 
 let error_with_module () =
-  error "Unsupported 'with' constraint in module implementation"
+  user_err Pp.(str "Unsupported 'with' constraint in module implementation")
 
 let is_functor = function
   | MoreFunctor _ -> true
@@ -49,7 +51,7 @@ let destr_functor = function
   | NoFunctor _ -> error_not_a_functor ()
 
 let module_body_of_type mp mtb =
-  { mtb with mod_mp = mp; mod_expr = Abstract }
+  { mtb with mod_mp = mp; mod_expr = Abstract; mod_retroknowledge = ModBodyRK [] }
 
 let rec add_structure mp sign resolver env =
   let add_one env (l,elem) =
@@ -83,27 +85,29 @@ let strengthen_const mp_from l cb resolver =
     | Def _ -> cb
     | _ ->
       let con = Constant.make2 mp_from l in
-      let u = 
-	if cb.const_polymorphic then
-	  Univ.make_abstract_instance cb.const_universes
-	else Univ.Instance.empty
+      let u =
+        match cb.const_universes with
+      | Monomorphic_const _ -> Univ.Instance.empty
+      | Polymorphic_const auctx -> Univ.make_abstract_instance auctx
       in
       { 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
-  else strengthen_body true mp_from mp_to mb
+  else
+    let mk_expr mp_to = Algebraic (NoFunctor (MEident mp_to)) in
+    strengthen_body mk_expr mp_from mp_to mb
 
-and strengthen_body is_mod mp_from mp_to mb =
+and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a generic_module_body =
+  fun mk_expr mp_from mp_to mb ->
   match mb.mod_type with
   | MoreFunctor _ -> mb
   | NoFunctor sign ->
     let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta
     in
     { mb with
-      mod_expr =
-        (if is_mod then Algebraic (NoFunctor (MEident mp_to)) else Abstract);
+      mod_expr = mk_expr mp_to;
       mod_type = NoFunctor sign_out;
       mod_delta = resolve_out }
 
@@ -130,7 +134,7 @@ and strengthen_sig mp_from sign mp_to resolver =
 	resolve_out,item::rest'
 
 let strengthen mtb mp =
-  strengthen_body false mtb.mod_mp mp mtb
+  strengthen_body ignore mtb.mod_mp mp mtb
 
 let subst_and_strengthen mb mp =
   strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
@@ -138,9 +142,9 @@ let subst_and_strengthen mb mp =
 let module_type_of_module mp mb =
   let mtb =
     { mb with
-      mod_expr = Abstract;
+      mod_expr = ();
       mod_type_alg = None;
-      mod_retroknowledge = [] }
+      mod_retroknowledge = ModTypeRK }
   in
   match mp with
   | Some mp -> strengthen {mtb with mod_mp = mp} mp
diff --git a/checker/modops.mli b/checker/modops.mli
index 26a088f3..9f6f7811 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
@@ -15,7 +17,7 @@ open Environ
 (* Various operations on modules and module types *)
 
 val module_type_of_module :
-  module_path option -> module_body -> module_type_body
+  ModPath.t option -> module_body -> module_type_body
 
 val is_functor : ('ty,'a) functorize -> bool
 
@@ -24,24 +26,24 @@ val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize
 (* adds a module and its components, but not the constraints *)
 val add_module : module_body ->  env -> env
 
-val add_module_type : module_path -> module_type_body -> env -> env
+val add_module_type : ModPath.t -> module_type_body -> env -> env
 
-val strengthen : module_type_body -> module_path -> module_type_body
+val strengthen : module_type_body -> ModPath.t -> module_type_body
 
-val subst_and_strengthen : module_body -> module_path -> module_body
+val subst_and_strengthen : module_body -> ModPath.t -> module_body
 
 val error_incompatible_modtypes :
   module_type_body -> module_type_body -> 'a
 
-val error_not_match : label -> structure_field_body -> 'a
+val error_not_match : Label.t -> structure_field_body -> 'a
 
 val error_with_module : unit -> 'a
 
-val error_no_such_label : label -> 'a
+val error_no_such_label : Label.t -> 'a
 
 val error_no_such_label_sub :
-  label -> module_path -> 'a
+  Label.t -> ModPath.t -> 'a
 
-val error_not_a_constant : label -> 'a
+val error_not_a_constant : Label.t -> 'a
 
-val error_not_a_module : label -> 'a
+val error_not_a_module : Label.t -> 'a
diff --git a/checker/print.ml b/checker/print.ml
index 7ef752b0..fc9cd687 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -1,146 +1,96 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Format
 open Cic
 open Names
 
-let chk_pp = Pp.pp_with Format.std_formatter
+let chk_pp fmt = Pp.pp_with fmt
+let pp_arrayi pp fmt a = Array.iteri (fun i x -> pp fmt (i,x)) a
+let pp_instance fmt i = chk_pp fmt (Univ.Instance.pr i)
+let pp_id fmt id = fprintf fmt "%s" (Id.to_string id)
 
-let print_instance i = chk_pp (Univ.Instance.pr i)
-
-let print_pure_constr csr =
-  let rec term_display c = match  c with
-  | Rel n -> print_string "#"; print_int n
-  | Meta n -> print_string "Meta("; print_int n; print_string ")"
-  | Var id -> print_string (Id.to_string id)
-  | Sort s -> sort_display s
-  | Cast (c,_, t) -> open_hovbox 1;
-      print_string "("; (term_display c); print_cut();
-      print_string "::"; (term_display t); print_string ")"; close_box()
+let print_pure_constr fmt csr =
+  let rec pp_term fmt c = match  c with
+  | Rel n  -> fprintf fmt "#%d" n
+  | Meta n -> fprintf fmt "Meta(%d)" n
+  | Var id -> pp_id fmt id
+  | Sort s -> pp_sort fmt s
+  | Cast (c,_, t) ->
+    fprintf fmt "@[<hov 1>(%a@;::%a)@]" pp_term c pp_term t
   | Prod (Name(id),t,c) ->
-      open_hovbox 1;
-      print_string"("; print_string (Id.to_string id);
-      print_string ":"; box_display t;
-      print_string ")"; print_cut();
-      box_display c; close_box()
+    fprintf fmt "@[<hov 1>(%a:%a)@;@[%a@]@]" pp_id id pp_term t pp_term c
   | Prod (Anonymous,t,c) ->
-      print_string"("; box_display t; print_cut(); print_string "->";
-      box_display c; print_string ")";
+    fprintf fmt "(%a@,->@[%a@])" pp_term t pp_term c
   | Lambda (na,t,c) ->
-      print_string "["; name_display na;
-      print_string ":"; box_display t; print_string "]";
-      print_cut(); box_display c;
+    fprintf fmt "[%a:@[%a@]]@,@[%a@]" pp_name na pp_term t pp_term c
   | LetIn (na,b,t,c) ->
-      print_string "["; name_display na; print_string "=";
-      box_display b; print_cut();
-      print_string ":"; box_display t; print_string "]";
-      print_cut(); box_display c;
+    fprintf fmt "[%a=@[%a@]@,:@[%a@]]@,@[%a@]" pp_name na pp_term b pp_term t pp_term c
   | App (c,l) ->
-      print_string "(";
-      box_display c;
-      Array.iter (fun x -> print_space (); box_display x) l;
-      print_string ")"
-  | Evar _ -> print_string "Evar#"
-  | Const (c,u) -> print_string "Cons(";
-      sp_con_display c;
-      print_string ","; print_instance u;
-      print_string ")"
+    fprintf fmt "(@[%a@]@, @[<hov 1>%a@])" pp_term c (pp_arrayi (fun _ (_,s) -> fprintf fmt "@[%a@]@," pp_term s)) l;
+  | Evar _ -> pp_print_string fmt "Evar#"
+  | Const (c,u) ->
+    fprintf fmt "Cons(@[%a,%a@])" sp_con_display c pp_instance u
   | Ind ((sp,i),u) ->
-      print_string "Ind(";
-      sp_display sp;
-      print_string ","; print_int i;
-      print_string ","; print_instance u;
-      print_string ")"
+    fprintf fmt "Ind(@[%a,%d,%a@])" sp_display sp i pp_instance u
   | Construct (((sp,i),j),u) ->
-      print_string "Constr(";
-      sp_display sp;
-      print_string ",";
-      print_int i; print_string ","; print_int j; 
-      print_string ","; print_instance u; print_string ")"
+    fprintf fmt "Constr(%a,%d,%d,%a)" sp_display sp i j pp_instance u
   | Case (ci,p,c,bl) ->
-      open_vbox 0;
-      print_string "<"; box_display p; print_string ">";
-      print_cut(); print_string "Case";
-      print_space(); box_display c; print_space (); print_string "of";
-      open_vbox 0;
-      Array.iter (fun x ->  print_cut();  box_display x) bl;
-      close_box();
-      print_cut();
-      print_string "end";
-      close_box()
+    let pp_match fmt (_,mc) = fprintf fmt " @[%a@]" pp_term mc in
+    fprintf fmt "@[<v><@[%a@]>@,Case@ @[%a@]@ of@[<v>%a@]@,end@]" pp_term p pp_term c (pp_arrayi pp_match) bl
   | Fix ((t,i),(lna,tl,bl)) ->
-      print_string "Fix("; print_int i; print_string ")";
-      print_cut();
-      open_vbox 0;
-      let print_fix () =
-        for k = 0 to (Array.length tl) - 1 do
-	  open_vbox 0;
-	  name_display lna.(k); print_string "/";
-	  print_int t.(k); print_cut(); print_string ":";
-	  box_display tl.(k) ; print_cut(); print_string ":=";
-	  box_display bl.(k); close_box ();
-	  print_cut()
-        done
-      in print_string"{"; print_fix(); print_string"}"
+    let pp_fixc fmt (k,_) =
+      fprintf fmt "@[<v 0> %a/%d@,:@[%a@]@,:=@[%a@]@]@," pp_name lna.(k) t.(k) pp_term tl.(k) pp_term bl.(k) in
+    fprintf fmt "Fix(%d)@,@[<v>{%a}@]" i (pp_arrayi pp_fixc) tl
   | CoFix(i,(lna,tl,bl)) ->
-      print_string "CoFix("; print_int i; print_string ")";
-      print_cut();
-      open_vbox 0;
-      let print_fix () =
-        for k = 0 to (Array.length tl) - 1 do
-          open_vbox 1;
-	  name_display lna.(k);  print_cut(); print_string ":";
-	  box_display tl.(k) ; print_cut(); print_string ":=";
-	  box_display bl.(k); close_box ();
-	  print_cut();
-        done
-      in print_string"{"; print_fix (); print_string"}"
+    let pp_fixc fmt (k,_) =
+      fprintf fmt "@[<v 0> %a@,:@[%a@]@,:=@[%a@]@]@," pp_name lna.(k) pp_term tl.(k) pp_term bl.(k) in
+    fprintf fmt "CoFix(%d)@,@[<v>{%a}@]" i (pp_arrayi pp_fixc) tl
   | Proj (p, c) ->
-    print_string "Proj("; sp_con_display (Projection.constant p); print_string ","; 
-    box_display c; print_string ")"
+    fprintf fmt "Proj(%a,@,@[%a@])" sp_con_display (Projection.constant p) pp_term c
 
-  and box_display c = open_hovbox 1; term_display c; close_box()
+  and pp_sort fmt = function
+    | Prop(Pos) -> pp_print_string fmt  "Set"
+    | Prop(Null) -> pp_print_string fmt "Prop"
+    | Type u -> fprintf fmt "Type(%a)" chk_pp (Univ.pr_uni u)
 
-  and sort_display = function
-    | Prop(Pos) -> print_string "Set"
-    | Prop(Null) -> print_string "Prop"
-    | Type u -> print_string "Type("; chk_pp (Univ.pr_uni u); print_string ")"
+  and pp_name fmt = function
+    | Name id -> pp_id fmt id
+    | Anonymous -> pp_print_string fmt "_"
 
-  and name_display = function
-    | Name id -> print_string (Id.to_string id)
-    | Anonymous -> print_string "_"
 (* Remove the top names for library and Scratch to avoid long names *)
-  and sp_display sp =
-(*    let dir,l = decode_kn sp in
+  and sp_display fmt sp =
+(*  let dir,l = decode_kn sp in
     let ls =
       match List.rev_map Id.to_string (DirPath.repr dir) with
           ("Top"::l)-> l
 	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (MutInd.debug_to_string sp)
-  and sp_con_display sp =
-(*    let dir,l = decode_kn sp in
+    pp_print_string fmt (MutInd.debug_to_string sp)
+
+  and sp_con_display fmt sp =
+    (*
+    let dir,l = decode_kn sp in
     let ls =
       match List.rev_map Id.to_string (DirPath.repr dir) with
           ("Top"::l)-> l
 	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (Constant.debug_to_string sp)
+    pp_print_string fmt (Constant.debug_to_string sp)
 
   in
-    try
-     box_display csr; print_flush()
-    with e ->
-	print_string (Printexc.to_string e);print_flush ();
-	raise e
-
-
-
+  try
+    fprintf fmt "@[%a@]%!" pp_term csr
+  with e ->
+    pp_print_string fmt (Printexc.to_string e);
+    print_flush ();
+    raise e
diff --git a/checker/print.mli b/checker/print.mli
new file mode 100644
index 00000000..da1362ca
--- /dev/null
+++ b/checker/print.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Cic
+
+val print_pure_constr : Format.formatter -> constr -> unit
diff --git a/checker/reduction.ml b/checker/reduction.ml
index ec16aa26..4e508dc7 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -1,11 +1,14 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Names
 open CErrors
 open Util
 open Cic
@@ -42,8 +45,8 @@ let compare_stack_shape stk1 stk2 =
     | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
     | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
-    | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1,
-       (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) ->
+    | ((ZcaseT(c1,_,_,_))::s1,
+       (ZcaseT(c2,_,_,_))::s2) ->
         bal=0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
     | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
         bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
@@ -52,7 +55,7 @@ let compare_stack_shape stk1 stk2 =
 
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
-  | Zlproj of Names.projection * lift
+  | Zlproj of Names.Projection.t * 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
@@ -78,8 +81,7 @@ let pure_stack lfts stk =
                 (l, Zlfix((lfx,fx),pa)::pstk)
             | (ZcaseT(ci,p,br,env),(l,pstk)) ->
                 (l,Zlcase(ci,l,mk_clos env p,mk_clos_vect env br)::pstk)
-            | (Zcase(ci,p,br),(l,pstk)) ->
-                (l,Zlcase(ci,l,p,br)::pstk)) in
+            ) in
   snd (pure_rec lfts stk)
 
 (****************************************************************************)
@@ -117,6 +119,10 @@ let beta_appvect c v =
 (*                         Conversion                               *)
 (********************************************************************)
 
+type conv_pb =
+  | CONV
+  | CUMUL
+
 (* Conversion utility functions *)
 type 'a conversion_function = env -> 'a -> 'a -> unit
 
@@ -137,7 +143,7 @@ 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
+               if not (Names.Constant.UserOrd.equal
 		       (Names.Projection.constant c1)
 		       (Names.Projection.constant c2)) then 
 		raise NotConvertible
@@ -152,11 +158,55 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
     cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2)
   else raise NotConvertible
 
-(* Convertibility of sorts *)
+let convert_inductive_instances cv_pb cumi u u' univs =
+  let len_instance =
+      Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in
+  if not ((len_instance = Univ.Instance.length u) &&
+          (len_instance = Univ.Instance.length u')) then
+    anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  else
+    let variance = Univ.ACumulativityInfo.variance cumi in
+    let comp_cst =
+      match cv_pb with
+      | CONV ->
+        Univ.Variance.eq_constraints variance u u' Univ.Constraint.empty
+      | CUMUL ->
+        Univ.Variance.leq_constraints variance u u' Univ.Constraint.empty
+    in
+    if (Univ.check_constraints comp_cst univs) then () else raise NotConvertible
+
+let convert_inductives
+    cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
+  match mind.mind_universes with
+  | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
+  | Cumulative_ind cumi ->
+    let num_param_arity =
+      mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+    in
+    if not (num_param_arity = sv1 && num_param_arity = sv2) then
+      convert_universes univs u1 u2
+    else
+      convert_inductive_instances cv_pb cumi u1 u2 univs
+
+let convert_constructors
+    (mind, ind, cns) u1 sv1 u2 sv2 univs =
+  match mind.mind_universes with
+  | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
+  | Cumulative_ind cumi ->
+    let num_cnstr_args =
+      let nparamsctxt =
+        mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+      in
+      nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
+    in
+    if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+      convert_universes univs u1 u2
+    else
+      (** By invariant, both constructors have a common supertype,
+          so they are convertible _at that type_. *)
+      ()
 
-type conv_pb =
-  | CONV
-  | CUMUL
+(* Convertibility of sorts *)
 
 let sort_cmp env univ pb s0 s1 =
   match (s0,s1) with
@@ -176,9 +226,9 @@ let sort_cmp env univ pb s0 s1 =
         then begin
           if !Flags.debug then begin
             let op = match pb with CONV -> "=" | CUMUL -> "<=" in
-            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))
+            Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
+               str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
+               ++ Univ.pr_universes univ)
           end;
           raise NotConvertible
         end
@@ -190,7 +240,6 @@ let rec no_arg_available = function
   | Zshift _ :: stk -> no_arg_available stk
   | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk
   | Zproj _ :: _ -> true
-  | Zcase _ :: _ -> true
   | ZcaseT _ :: _ -> true
   | Zfix _ :: _ -> true
 
@@ -203,7 +252,6 @@ let rec no_nth_arg_available n = function
       if n >= k then no_nth_arg_available (n-k) stk
       else false
   | Zproj _ :: _ -> true
-  | Zcase _ :: _ -> true
   | ZcaseT _ :: _ -> true
   | Zfix _ :: _ -> true
 
@@ -213,13 +261,12 @@ let rec no_case_available = function
   | Zshift _ :: stk -> no_case_available stk
   | Zapp _ :: stk -> no_case_available stk
   | Zproj (_,_,_) :: _ -> false
-  | Zcase _ :: _ -> false
   | ZcaseT _ :: _ -> false
   | Zfix _ :: _ -> true
 
 let in_whnf (t,stk) =
   match fterm_of t with
-    | (FLetIn _ | FCase _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false
+    | (FLetIn _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false
     | FLambda _ -> no_arg_available stk
     | FConstruct _ -> no_case_available stk
     | FCoFix _ -> no_case_available stk
@@ -227,16 +274,34 @@ let in_whnf (t,stk) =
     | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true
     | FLOCKED -> assert false
 
-let oracle_order fl1 fl2 =
-  match fl1,fl2 with
-      ConstKey c1, ConstKey c2 -> (*height c1 > height c2*)false
-    | _, ConstKey _ -> true
-    | _ -> false
-
-let unfold_projection infos p c =
-  let pb = lookup_projection p (infos_env infos) in
-  let s = Zproj (pb.proj_npars, pb.proj_arg, p) in
-    (c, s)
+let default_level = Level 0
+
+let get_strategy { var_opacity; cst_opacity } = function
+  | VarKey id ->
+      (try Names.Id.Map.find id var_opacity
+      with Not_found -> default_level)
+  | ConstKey (c, _) ->
+      (try Names.Cmap.find c cst_opacity
+      with Not_found -> default_level)
+  | RelKey _ -> Expand
+
+let oracle_order infos l2r k1 k2 =
+  let o = Closure.oracle_of_infos infos in
+  match get_strategy o k1, get_strategy o k2 with
+  | Expand, Expand -> l2r
+  | Expand, (Opaque | Level _) -> true
+  | (Opaque | Level _), Expand -> false
+  | Opaque, Opaque -> l2r
+  | Level _, Opaque -> true
+  | Opaque, Level _ -> false
+  | Level n1, Level n2 ->
+     if Int.equal n1 n2 then l2r
+     else n1 < n2
+
+let eq_table_key univ =
+  Names.eq_table_key (fun (c1,u1) (c2,u2) ->
+      Constant.UserOrd.equal c1 c2 &&
+      Univ.Instance.check_eq univ u1 u2)
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
@@ -284,13 +349,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
     (* 2 constants, 2 local defined vars or 2 defined rels *)
     | (FFlex fl1, FFlex fl2) ->
 	(try (* try first intensional equality *)
-	  if eq_table_key fl1 fl2
+          if eq_table_key univ fl1 fl2
           then convert_stacks univ infos lft1 lft2 v1 v2
           else raise NotConvertible
         with NotConvertible ->
           (* else the oracle tells which constant is to be expanded *)
           let (app1,app2) =
-            if oracle_order fl1 fl2 then
+            if oracle_order infos false fl1 fl2 then
               match unfold_reference infos fl1 with
               | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
               | None ->
@@ -307,12 +372,12 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
             eqappr univ cv_pb infos app1 app2)
 	  
     | (FProj (p1,c1), _) ->
-      let (def1, s1) = unfold_projection infos p1 c1 in
-        eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2
+      let s1 = unfold_projection (infos_env infos) p1 in
+        eqappr univ cv_pb infos (lft1, whd_stack infos c1 (s1 :: v1)) appr2
 	  
     | (_, FProj (p2,c2)) ->
-      let (def2, s2) = unfold_projection infos p2 c2 in
-        eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2))
+      let s2 = unfold_projection (infos_env infos) p2 in
+        eqappr univ cv_pb infos appr1 (lft2, whd_stack infos c2 (s2 :: v2))
 
     (* other constructors *)
     | (FLambda _, FLambda _) ->
@@ -333,13 +398,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
     (* Eta-expansion on the fly *)
     | (FLambda _, _) ->
         if v1 <> [] then
-          anomaly (Pp.str "conversion was given unreduced term (FLambda)");
+          anomaly (Pp.str "conversion was given unreduced term (FLambda).");
         let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
         eqappr univ CONV infos
           (el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2))
     | (_, FLambda _) ->
         if v2 <> [] then
-          anomaly (Pp.str "conversion was given unreduced term (FLambda)");
+          anomaly (Pp.str "conversion was given unreduced term (FLambda).");
         let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
         eqappr univ CONV infos
           (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[]))
@@ -375,18 +440,37 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
-        if mind_equiv_infos infos ind1 ind2
-	then
-	  (let () = convert_universes univ u1 u2 in
-           convert_stacks univ infos lft1 lft2 v1 v2)
-        else raise NotConvertible
-
-     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
-	 if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2
-	 then
-	  (let () = convert_universes univ u1 u2 in
-           convert_stacks univ infos lft1 lft2 v1 v2)
-         else raise NotConvertible
+      if mind_equiv_infos infos ind1 ind2 then
+        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+          begin
+            convert_universes univ u1 u2;
+            convert_stacks univ infos lft1 lft2 v1 v2
+          end
+        else
+          let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+          let () =
+            convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
+              u2 (stack_args_size v2) univ
+          in
+          convert_stacks univ infos lft1 lft2 v1 v2
+      else raise NotConvertible
+
+    | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
+      if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then
+        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+          begin
+            convert_universes univ u1 u2;
+            convert_stacks univ infos lft1 lft2 v1 v2
+          end
+        else
+          let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+          let () =
+            convert_constructors
+              (mind, snd ind1, j1) u1 (stack_args_size v1)
+              u2 (stack_args_size v2) univ
+          in
+          convert_stacks univ infos lft1 lft2 v1 v2
+      else raise NotConvertible
 
      (* Eta expansion of records *)
      | (FConstruct ((ind1,j1),u1), _) ->
@@ -432,8 +516,8 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
          else raise NotConvertible
 
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
-     | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
-       | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
+     | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
+       | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
        | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
 
      (* In all other cases, terms are not convertible *)
@@ -479,7 +563,7 @@ let vm_conv cv_pb = fconv cv_pb true
 let hnf_prod_app env t n =
   match whd_all env t with
     | Prod (_,_,b) -> subst1 n b
-    | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
+    | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.")
 
 let hnf_prod_applist env t nl =
   List.fold_left (hnf_prod_app env) t nl
@@ -508,7 +592,6 @@ let dest_prod_assum env =
     | LetIn (x,b,t,c) ->
         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_all env rty in
 	if Term.eq_constr rty' rty then l, rty
@@ -526,7 +609,6 @@ let dest_lam_assum env =
     | LetIn (x,b,t,c) ->
         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
   in
   lamec_rec env empty_rel_context
@@ -536,5 +618,5 @@ let dest_arity env c =
   let l, c = dest_prod_assum env c in
   match c with
     | Sort s -> l,s
-    | _ -> error "not an arity"
+    | _ -> user_err Pp.(str "not an arity")
 
diff --git a/checker/reduction.mli b/checker/reduction.mli
index 15a2df1f..3bbf4654 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 11cd742b..e3640c37 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Pp
@@ -40,7 +42,7 @@ let check_engagement env expected_impredicative_set =
   begin
     match impredicative_set, expected_impredicative_set with
     | PredicativeSet, ImpredicativeSet ->
-        CErrors.error "Needs option -impredicative-set."
+        CErrors.user_err Pp.(str "Needs option -impredicative-set.")
     | _ -> ()
   end;
   ()
@@ -61,7 +63,7 @@ let check_imports f caller env needed =
       let actual_stamp = lookup_digest env dp in
       if stamp <> actual_stamp then report_clash f caller dp
     with Not_found ->
-      error ("Reference to unknown module " ^ (DirPath.to_string dp))
+      user_err Pp.(str ("Reference to unknown module " ^ (DirPath.to_string dp)))
   in
   Array.iter check needed
 
@@ -89,6 +91,6 @@ let import file clib univs digest =
 let unsafe_import file clib univs digest =
   let env = !genv in
   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;
+  else check_imports (user_err ~hdr:"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/safe_typing.mli b/checker/safe_typing.mli
index 8724f8e0..51e5ca32 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 7eae9b83..31dab0c9 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -1,13 +1,14 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
-open CErrors
 open Util
 open Names
 open Cic
@@ -81,6 +82,14 @@ let check_conv_error error f env a1 a2 =
   with
       NotConvertible -> error ()
 
+let check_polymorphic_instance error env auctx1 auctx2 =
+  if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then
+    error ()
+  else if not (Univ.check_subtype (Environ.universes env) auctx2 auctx1) then
+    error ()
+  else
+    Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
+
 (* for now we do not allow reorderings *)
 let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2= 
   let kn = MutInd.make2 mp1 l in
@@ -88,18 +97,31 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   let check_conv f = check_conv_error error f in
   let mib1 =
     match info1 with
-      | IndType ((_,0), mib) -> mib
+      | IndType ((_,0), mib) -> subst_mind subst1 mib
       | _ -> error ()
   in
   let mib2 = subst_mind subst2 mib2 in
   let check eq f = if not (eq (f mib1) (f mib2)) then error () in
-  let bool_equal (x : bool) (y : bool) = x = y in
-  let u = 
-    check bool_equal (fun x -> x.mind_polymorphic);
-    if mib1.mind_polymorphic then (
-      check Univ.Instance.equal (fun x -> Univ.UContext.instance x.mind_universes);
-      Univ.UContext.instance mib1.mind_universes)
-    else Univ.Instance.empty
+  let env, u =
+    match mib1.mind_universes, mib2.mind_universes with
+    | Monomorphic_ind _, Monomorphic_ind _ -> env, Univ.Instance.empty
+    | Polymorphic_ind auctx, Polymorphic_ind auctx' ->
+      let env = check_polymorphic_instance error env auctx auctx' in
+      env, Univ.make_abstract_instance auctx'
+    | Cumulative_ind cumi, Cumulative_ind cumi' ->
+      (** Currently there is no way to control variance of inductive types, but
+          just in case we require that they are in a subtyping relation. *)
+      let () =
+        let v = Univ.ACumulativityInfo.variance cumi in
+        let v' = Univ.ACumulativityInfo.variance cumi' in
+        if not (Array.for_all2 Univ.Variance.check_subtype v' v) then
+          CErrors.anomaly Pp.(str "Variance mismatch for " ++ MutInd.print kn)
+      in
+      let auctx = Univ.ACumulativityInfo.univ_context cumi in
+      let auctx' = Univ.ACumulativityInfo.univ_context cumi' in
+      let env = check_polymorphic_instance error env auctx auctx' in
+      env, Univ.make_abstract_instance auctx'
+    | _ -> error ()
   in
   let eq_projection_body p1 p2 =
     let check eq f = if not (eq (f p1) (f p2)) then error () in
@@ -111,40 +133,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     check (eq_constr) (fun x -> snd x.proj_eta);
     check (eq_constr) (fun x -> x.proj_body); true
   in
-  let check_inductive_type env t1 t2 =
-
-    (* Due to sort-polymorphism in inductive types, the conclusions of
-       t1 and t2, if in Type, are generated as the least upper bounds
-       of the types of the constructors.
-
-       By monotonicity of the infered l.u.b.  wrt subtyping (i.e.  if X:U
-       |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each
-       universe in the conclusion of t1 has an bounding universe in
-       the conclusion of t2, so that we don't need to check the
-       subtyping of the conclusions of t1 and t2.
-
-       Even if we'd like to recheck it, the inference of constraints
-       is not designed to deal with algebraic constraints of the form
-       max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy
-       to recheck it (in short, we would need the actual graph of
-       constraints as input while type checking is currently designed
-       to output a set of constraints instead) *)
-
-    (* So we cheat and replace the subtyping problem on algebraic
-       constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n)
-       (that we know are necessary true) by trivial constraints that
-       the constraint generator knows how to deal with *)
-
-    let (ctx1,s1) = dest_arity env t1 in
-    let (ctx2,s2) = dest_arity env t2 in
-    let s1,s2 =
-      match s1, s2 with
-      | Type _, Type _ -> (* shortcut here *) Prop Null, Prop Null
-      | (Prop _, Type _) | (Type _,Prop _) -> error ()
-      | _ -> (s1, s2) in
-    check_conv conv_leq env
-      (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
-  in
+  let check_inductive_type t1 t2 = check_conv conv_leq env t1 t2 in
 
   let check_packet p1 p2 =
     let check eq f = if not (eq (f p1) (f p2)) then error () in
@@ -163,8 +152,8 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       (* nparams done *)
       (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      check_inductive_type env
-        (type_of_inductive env ((mib1,p1),u)) (type_of_inductive env ((mib2,p2),u))
+      check_inductive_type
+        (type_of_inductive env ((mib1,p1), u)) (type_of_inductive env ((mib2,p2),u))
   in
   let check_cons_types i p1 p2 =
     Array.iter2 (check_conv conv env)
@@ -201,7 +190,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     | Some None, Some None -> true
     | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) ->
       Id.equal id1 id2 &&
-      Array.for_all2 eq_con_chk p1 p2 &&
+      Array.for_all2 Constant.UserOrd.equal p1 p2 &&
       Array.for_all2 eq_projection_body pb1 pb2
     | _, _ -> false
   in
@@ -230,59 +219,25 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
 let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
   let error () = error_not_match l spec2 in
   let check_conv f = check_conv_error error f in
-  let check_type env t1 t2 =
-
-    (* If the type of a constant is generated, it may mention
-       non-variable algebraic universes that the general conversion
-       algorithm is not ready to handle. Anyway, generated types of
-       constants are functions of the body of the constant. If the
-       bodies are the same in environments that are subtypes one of
-       the other, the types are subtypes too (i.e. if Gamma <= Gamma',
-       Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
-       Hence they don't have to be checked again *)
-
-    let t1,t2 =
-      if isArity t2 then
-        let (ctx2,s2) = destArity t2 in
-        match s2 with
-        | Type v when not (Univ.is_univ_variable v) ->
-          (* The type in the interface is inferred and is made of algebraic
-             universes *)
-          begin try
-            let (ctx1,s1) = dest_arity env t1 in
-            match s1 with
-            | Type u when not (Univ.is_univ_variable u) ->
-              (* Both types are inferred, no need to recheck them. We
-                 cheat and collapse the types to Prop *)
-                mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
-            | Prop _ ->
-              (* The type in the interface is inferred, it may be the case
-                 that the type in the implementation is smaller because
-                 the body is more reduced. We safely collapse the upper
-                 type to Prop *)
-                mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
-            | Type _ ->
-              (* The type in the interface is inferred and the type in the
-                 implementation is not inferred or is inferred but from a
-                 more reduced body so that it is just a variable. Since
-                 constraints of the form "univ <= max(...)" are not
-                 expressible in the system of algebraic universes: we fail
-                 (the user has to use an explicit type in the interface *)
-                error ()
-          with UserError _ (* "not an arity" *) ->
-            error () end
-        | _ -> t1,t2
-      else
-        (t1,t2) in
-    check_conv conv_leq env t1 t2
-  in
+  let check_type env t1 t2 = check_conv conv_leq env t1 t2 in
     match info1 with
       | Constant cb1 ->
 	let cb1 = subst_const_body subst1 cb1 in
 	let cb2 = subst_const_body subst2 cb2 in
-	(*Start by checking types*)
-	let typ1 = Typeops.type_of_constant_type env cb1.const_type in
-	let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+        (*Start by checking universes *)
+        let env =
+          match cb1.const_universes, cb2.const_universes with
+          | Monomorphic_const _, Monomorphic_const _ -> env
+          | Polymorphic_const auctx1, Polymorphic_const auctx2 ->
+            check_polymorphic_instance error env auctx1 auctx2
+          | Monomorphic_const _, Polymorphic_const _ ->
+            error ()
+          | Polymorphic_const _, Monomorphic_const _ ->
+            error ()
+        in
+        (* Now check types *)
+	let typ1 = cb1.const_type in
+	let typ2 = cb2.const_type in
 	check_type env typ1 typ2;
 	(* Now we check the bodies:
 	 - A transparent constant can only be implemented by a compatible
@@ -302,27 +257,17 @@ 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 (CErrors.error (
+        CErrors.user_err (Pp.str (
 		    "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 " ^
-		      "name."));
-      if constant_has_body cb2 then error () ;
-      let u = inductive_instance mind1 in
-      let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in
-      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 (CErrors.error (
+		      "name."))
+   | IndConstr (((kn,i),j),mind1) ->
+      CErrors.user_err (Pp.str (
        "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 " ^
-       "name."));
-      if constant_has_body cb2 then error () ;
-      let u1 = inductive_instance mind1 in
-      let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
-      let ty2 = Typeops.type_of_constant_type env cb2.const_type in
-       check_conv conv env ty1 ty2
+       "name."))
 
 let rec check_modules  env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module None msb1 in
@@ -390,7 +335,7 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
 			  mod_type = body_t1;
 			  mod_type_alg = None;
 			  mod_constraints = mtb1.mod_constraints;
-			  mod_retroknowledge = [];
+			  mod_retroknowledge = ModBodyRK [];
 			  mod_delta = mtb1.mod_delta} env
 	  in
 	  check_structure env body_t1 body_t2 equiv
diff --git a/checker/subtyping.mli b/checker/subtyping.mli
index cc66fc53..bb867186 100644
--- a/checker/subtyping.mli
+++ b/checker/subtyping.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
diff --git a/checker/term.ml b/checker/term.ml
index 591348cb..0236f786 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -1,12 +1,14 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(* This module instantiates the structure of generic deBruijn terms to Coq *)
+(* This module instantiates the structure of generic de Bruijn terms to Coq *)
 
 open CErrors
 open Util
@@ -94,7 +96,7 @@ let closedn n c =
   in
   try closed_rec n c; true with LocalOccur -> false
 
-(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+(* [closed0 M] is true iff [M] is a (de Bruijn) closed term *)
 
 let closed0 = closedn 0
 
@@ -227,6 +229,8 @@ let rel_context_nhyps hyps =
   nhyps 0 hyps
 let fold_rel_context f l ~init = List.fold_right f l init
 
+let fold_rel_context_outside f l ~init = List.fold_right f l init
+
 let map_rel_decl f = function
   | LocalAssum (n, typ) as decl ->
      let typ' = f typ in
@@ -273,14 +277,14 @@ let decompose_lam =
   abstractions *)
 let decompose_lam_n_assum n =
   if n < 0 then
-    error "decompose_lam_n_assum: integer parameter must be positive";
+    user_err Pp.(str "decompose_lam_n_assum: integer parameter must be positive");
   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 (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"
+    | c -> user_err Pp.(str "decompose_lam_n_assum: not enough abstractions")
   in
   lamdec_rec empty_rel_context n
 
@@ -306,14 +310,14 @@ let decompose_prod_assum =
 
 let decompose_prod_n_assum n =
   if n < 0 then
-    error "decompose_prod_n_assum: integer parameter must be positive";
+    user_err Pp.(str "decompose_prod_n_assum: integer parameter must be positive");
   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 (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"
+    | c -> user_err Pp.(str "decompose_prod_n_assum: not enough assumptions")
   in
   prodec_rec empty_rel_context n
 
@@ -333,7 +337,7 @@ let destArity =
     | 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")
+    | _               -> anomaly ~label:"destArity" (Pp.str "not an arity.")
   in
   prodec_rec []
 
@@ -386,7 +390,7 @@ let compare_constr f t1 t2 =
           f h1 h2 && List.for_all2 f l1 l2
         else false
   | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2
-  | Const c1, Const c2 -> eq_puniverses eq_con_chk c1 c2
+  | Const c1, Const c2 -> eq_puniverses Constant.UserOrd.equal c1 c2
   | Ind c1, Ind c2 -> eq_puniverses eq_ind_chk c1 c2
   | Construct ((c1,i1),u1), Construct ((c2,i2),u2) -> Int.equal i1 i2 && eq_ind_chk c1 c2
     && Univ.Instance.equal u1 u2
@@ -414,35 +418,33 @@ let subst_instance_constr subst c =
   if Univ.Instance.is_empty subst then c
   else
     let f u = Univ.subst_instance_instance subst u in
-    let changed = ref false in
-    let rec aux t = 
+    let rec aux t =
       match t with
-      | Const (c, u) -> 
-	if Univ.Instance.is_empty u then t
-	else 
-          let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; Const (c, u'))
+      | Const (c, u) ->
+       if Univ.Instance.is_empty u then t
+       else
+          let u' = f u in
+           if u' == u then t
+           else (Const (c, u'))
       | Ind (i, u) ->
-	if Univ.Instance.is_empty u then t
-	else 
-	  let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; Ind (i, u'))
+       if Univ.Instance.is_empty u then t
+       else
+         let u' = f u in
+           if u' == u then t
+           else (Ind (i, u'))
       | Construct (c, u) ->
-	if Univ.Instance.is_empty u then t
-	else 
-          let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; Construct (c, u'))
-      | Sort (Type u) -> 
+       if Univ.Instance.is_empty u then t
+       else
+          let u' = f u in
+           if u' == u then t
+           else (Construct (c, u'))
+      | Sort (Type u) ->
          let u' = Univ.subst_instance_universe subst u in
-	   if u' == u then t else 
-	     (changed := true; Sort (sort_of_univ u'))
+          if u' == u then t else
+            (Sort (sort_of_univ u'))
       | _ -> map_constr aux t
     in
-    let c' = aux c in
-      if !changed then c' else c
+    aux c
 
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx
diff --git a/checker/term.mli b/checker/term.mli
index 0af83e05..2524dff1 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -4,8 +4,6 @@ open Cic
 val family_of_sort : sorts -> sorts_family
 val family_equal : sorts_family -> sorts_family -> bool
 
-val strip_outer_cast : constr -> constr
-val collapse_appl : constr -> constr
 val decompose_app : constr -> constr * constr list
 val applist : constr * constr list -> constr
 val iter_constr_with_binders :
@@ -35,11 +33,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 fold_rel_context_outside :
+  (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 compose_lam : (Name.t * constr) list -> constr -> constr
+val decompose_lam : constr -> (Name.t * constr) list * constr
 val decompose_lam_n_assum : int -> constr -> rel_context * constr
 val mkProd_or_LetIn : rel_declaration -> constr -> constr
 val it_mkProd_or_LetIn : constr -> rel_context -> constr
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index b7718e02..50796437 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Names
@@ -52,14 +54,14 @@ type type_error =
   | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
   | IllFormedBranch of constr * int * constr * constr
-  | Generalization of (name * constr) * unsafe_judgment
+  | Generalization of (Name.t * constr) * unsafe_judgment
   | ActualType of unsafe_judgment * constr
   | CantApplyBadType of
       (int * constr * constr) * unsafe_judgment * unsafe_judgment array
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
-  | IllFormedRecBody of guard_error * name array * int
+  | IllFormedRecBody of guard_error * Name.t array * int
   | IllTypedRecBody of
-      int * name array * unsafe_judgment array * constr array
+      int * Name.t array * unsafe_judgment array * constr array
   | UnsatisfiedConstraints of Univ.constraints
 
 exception TypeError of env * type_error
diff --git a/checker/type_errors.mli b/checker/type_errors.mli
index d9d14795..09703458 100644
--- a/checker/type_errors.mli
+++ b/checker/type_errors.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
@@ -54,14 +56,14 @@ type type_error =
   | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
   | IllFormedBranch of constr * int * constr * constr
-  | Generalization of (name * constr) * unsafe_judgment
+  | Generalization of (Name.t * constr) * unsafe_judgment
   | ActualType of unsafe_judgment * constr
   | CantApplyBadType of
       (int * constr * constr) * unsafe_judgment * unsafe_judgment array
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
-  | IllFormedRecBody of guard_error * name array * int
+  | IllFormedRecBody of guard_error * Name.t array * int
   | IllTypedRecBody of
-      int * name array * unsafe_judgment array * constr array
+      int * Name.t array * unsafe_judgment array * constr array
   | UnsatisfiedConstraints of Univ.constraints
 
 exception TypeError of env * type_error
@@ -96,9 +98,9 @@ val error_cant_apply_bad_type :
       unsafe_judgment -> unsafe_judgment array -> 'a
 
 val error_ill_formed_rec_body :
-  env -> guard_error -> name array -> int -> 'a
+  env -> guard_error -> Name.t array -> int -> 'a
 
 val error_ill_typed_rec_body  :
-  env -> int -> name array -> unsafe_judgment array -> constr array -> 'a
+  env -> int -> Name.t array -> unsafe_judgment array -> constr array -> 'a
 
 val error_unsatisfied_constraints : env -> Univ.constraints -> 'a
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 173e19ce..18f07dc0 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open CErrors
@@ -69,38 +71,16 @@ let judge_of_relative env n =
 
 (* Type of constants *)
 
-
-let type_of_constant_type_knowing_parameters env t paramtyps =
-  match t with
-  | RegularArity t -> t
-  | TemplateArity (sign,ar) ->
-      let ctx = List.rev sign in
-      let ctx,s = instantiate_universes env ctx ar paramtyps in
-      mkArity (List.rev ctx,s)
-
-let type_of_constant_knowing_parameters env cst paramtyps =
-  let ty, cu = constant_type env cst in
-    type_of_constant_type_knowing_parameters env ty paramtyps, cu
-
-let type_of_constant_type env t =
-  type_of_constant_type_knowing_parameters env t [||]
-
-let type_of_constant env cst =
-  type_of_constant_knowing_parameters env cst [||]
-
-let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp =
+let judge_of_constant env (kn,u as cst) =
   let _cb =
     try lookup_constant kn env
     with Not_found ->
       failwith ("Cannot find constant: "^Constant.to_string kn)
   in
-  let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in
+  let ty, cu = constant_type env cst in
   let () = check_constraints cu env in
     ty
 
-let judge_of_constant env cst =
-  judge_of_constant_knowing_parameters env cst [||]
-
 (* Type of an application. *)
 
 let judge_of_apply env (f,funj) argjv =
@@ -265,7 +245,7 @@ let rec execute env cstr =
 
     | Rel n -> judge_of_relative env n
 
-    | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
+    | Var _ -> anomaly (Pp.str "Section variable in Coqchk!")
 
     | Const c -> judge_of_constant env c
 
@@ -278,13 +258,9 @@ let rec execute env cstr =
 	let j =
 	  match f with
 	    | Ind ind ->
-		(* Sort-polymorphism of inductive types *)
 		judge_of_inductive_knowing_parameters env ind jl
-	    | Const cst ->
-		(* Sort-polymorphism of constant *)
-		judge_of_constant_knowing_parameters env cst jl
 	    | _ ->
-		(* No sort-polymorphism *)
+		(* No template polymorphism *)
 		execute env f
 	in
         let jl = Array.map2 (fun c ty -> c,ty) args jl in
@@ -334,7 +310,6 @@ let rec execute env cstr =
         let pj = execute env p in
         let lfj = execute_array env lf in
         judge_of_case env ci (p,pj) (c,cj) lfj
-
     | Fix ((_,i as vni),recdef) ->
         let fix_ty = execute_recdef env recdef i in
         let fix = (vni,recdef) in
@@ -349,10 +324,10 @@ let rec execute env cstr =
 
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
-	anomaly (Pp.str "the kernel does not support metavariables")
+	anomaly (Pp.str "the kernel does not support metavariables.")
 
     | Evar _ ->
-	anomaly (Pp.str "the kernel does not support existential variables")
+	anomaly (Pp.str "the kernel does not support existential variables.")
 
 and execute_type env constr =
   let j = execute env constr in
diff --git a/checker/typeops.mli b/checker/typeops.mli
index db8e467a..c2d7d19c 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
@@ -18,6 +20,3 @@ val infer_type : env -> constr      -> sorts
 val check_ctxt : env -> rel_context -> env
 val check_polymorphic_arity :
   env -> rel_context -> template_arity -> unit
-
-val type_of_constant_type : env -> constant_type -> constr
-
diff --git a/checker/univ.ml b/checker/univ.ml
index 668f3a05..1619010c 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Created in Caml by Gérard Huet for CoC 4.8 [Dec 1988] *)
@@ -29,114 +31,6 @@ open Util
    union-find algorithm. The assertions $<$ and $\le$ are represented by
    adjacency lists *)
 
-module type Hashconsed =
-sig
-  type t
-  val hash : t -> int
-  val eq : t -> t -> bool
-  val hcons : t -> t
-end
-
-module HashedList (M : Hashconsed) :
-sig
-  type t = private Nil | Cons of M.t * int * t
-  val nil : t
-  val cons : M.t -> t -> t
-end =
-struct
-  type t = Nil | Cons of M.t * int * t
-  module Self =
-  struct
-    type _t = t
-    type t = _t
-    type u = (M.t -> M.t)
-    let hash = function Nil -> 0 | Cons (_, h, _) -> h
-    let eq l1 l2 = match l1, l2 with
-    | Nil, Nil -> true
-    | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2
-    | _ -> false
-    let hashcons hc = function
-    | Nil -> Nil
-    | Cons (x, h, l) -> Cons (hc x, h, l)
-  end
-  module Hcons = Hashcons.Make(Self)
-  let hcons = Hashcons.simple_hcons Hcons.generate Hcons.hcons M.hcons
-  (** No recursive call: the interface guarantees that all HLists from this
-      program are already hashconsed. If we get some external HList, we can
-      still reconstruct it by traversing it entirely. *)
-  let nil = Nil
-  let cons x l =
-    let h = M.hash x in
-    let hl = match l with Nil -> 0 | Cons (_, h, _) -> h in
-    let h = Hashset.Combine.combine h hl in
-    hcons (Cons (x, h, l))
-end
-
-module HList = struct
-
-  module type S = sig
-    type elt
-    type t = private Nil | Cons of elt * int * t
-    val hash : t -> int
-    val nil : t
-    val cons : elt -> t -> t
-    val tip : elt -> t
-    val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
-    val map : (elt -> elt) -> t -> t
-    val smartmap : (elt -> elt) -> t -> t
-    val exists : (elt -> bool) -> t -> bool
-    val for_all : (elt -> bool) -> t -> bool
-    val for_all2 : (elt -> elt -> bool) -> t -> t -> bool
-    val remove : elt -> t -> t
-    val to_list : t -> elt list
-  end
-
-  module Make (H : Hashconsed) : S with type elt = H.t =
-  struct
-  type elt = H.t
-  include HashedList(H)
-
-  let hash = function Nil -> 0 | Cons (_, h, _) -> h
-
-  let tip e = cons e nil
-
-  let rec fold f l accu = match l with
-  | Nil -> accu
-  | Cons (x, _, l) -> fold f l (f x accu)
-
-  let rec map f = function
-  | Nil -> nil
-  | Cons (x, _, l) -> cons (f x) (map f l)
-
-  let smartmap = map
-  (** Apriori hashconsing ensures that the map is equal to its argument *)
-
-  let rec exists f = function
-  | Nil -> false
-  | Cons (x, _, l) -> f x || exists f l
-
-  let rec for_all f = function
-  | Nil -> true
-  | Cons (x, _, l) -> f x && for_all f l
-
-  let rec for_all2 f l1 l2 = match l1, l2 with
-  | Nil, Nil -> true
-  | Cons (x1, _, l1), Cons (x2, _, l2) -> f x1 x2 && for_all2 f l1 l2
-  | _ -> false
-
-  let rec to_list = function
-  | Nil -> []
-  | Cons (x, _, l) -> x :: to_list l
-
-  let rec remove x = function
-  | Nil -> nil
-  | Cons (y, _, l) ->
-    if H.eq x y then l
-    else cons y (remove x l)
-
-  end
-end
-
 module RawLevel =
 struct
   open Names
@@ -174,24 +68,6 @@ struct
     | _, Level _ -> 1
     | Var n, Var m -> Int.compare n m
 
-  let hequal x y =
-    x == y ||
-      match x, y with
-      | Prop, Prop -> true
-      | Set, Set -> true
-      | Level (n,d), Level (n',d') ->
-        n == n' && d == d'
-      | Var n, Var n' -> n == n'
-      | _ -> false
-
-  let hcons = function
-    | Prop as x -> x
-    | Set as x -> x
-    | Level (n,d) as x -> 
-      let d' = Names.DirPath.hcons d in
-        if d' == d then x else Level (n,d')
-    | Var n as x -> x
-
   open Hashset.Combine
 
   let hash = function
@@ -223,24 +99,7 @@ module Level = struct
 
   let data x = x.data
 
-  (** Hashcons on levels + their hash *)
-
-  module Self = struct
-    type _t = t
-    type t = _t
-    type u = unit
-    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
-      if x.data == data' then x else { x with data = data' }
-  end
-
-  let hcons =
-    let module H = Hashcons.Make(Self) in
-    Hashcons.simple_hcons H.generate H.hcons ()
-
-  let make l = hcons { hash = RawLevel.hash l; data = l }
+  let make l = { hash = RawLevel.hash l; data = l }
 
   let set = make Set
   let prop = make Prop
@@ -277,7 +136,7 @@ module Level = struct
 
   let pr u = str (to_string u)
 
-  let make m n = make (Level (n, Names.DirPath.hcons m))
+  let make m n = make (Level (n, m))
 
 end
 
@@ -310,48 +169,12 @@ struct
   module Expr = 
   struct
     type t = Level.t * int
-    type _t = t
 	
-    (* Hashing of expressions *)
-    module ExprHash = 
-    struct
-      type t = _t
-      type u = Level.t -> Level.t
-      let hashcons hdir (b,n as x) = 
-	let b' = hdir b in 
-	  if b' == b then x else (b',n)
-      let eq l1 l2 =
-        l1 == l2 || 
-        match l1,l2 with
-	| (b,n), (b',n') -> b == b' && n == n'
-
-      let hash (x, n) = n + Level.hash x
-
-    end
-
-    module HExpr =
-    struct
-
-      module H = Hashcons.Make(ExprHash)
-
-      type t = ExprHash.t
-
-      let hcons =
-        Hashcons.simple_hcons H.generate H.hcons Level.hcons
-      let hash = ExprHash.hash
-      let eq x y = x == y ||
-        (let (u,n) = x and (v,n') = y in
-           Int.equal n n' && Level.equal u v)
-
-    end
+    let make l = (l, 0)
 
-    let hcons = HExpr.hcons
-
-    let make l = hcons (l, 0)
-
-    let prop = make Level.prop
-    let set = make Level.set
-    let type1 = hcons (Level.set, 1)
+    let prop = (Level.prop, 0)
+    let set = (Level.set, 0)
+    let type1 = (Level.set, 1)
 
     let is_prop = function
       | (l,0) -> Level.is_prop l
@@ -361,22 +184,15 @@ struct
       (let (u,n) = x and (v,n') = y in
 	 Int.equal n n' && Level.equal u v)
 
-    let leq (u,n) (v,n') =
-      let cmp = Level.compare u v in
-	if Int.equal cmp 0 then n <= n'
-	else if n <= n' then 
-	  (Level.is_prop u && Level.is_small v)
-	else false
-
     let successor (u,n) =
       if Level.is_prop u then type1
-      else hcons (u, n + 1)
+      else (u, n + 1)
 
     let addn k (u,n as x) = 
       if k = 0 then x 
       else if Level.is_prop u then
-	hcons (Level.set,n+k)
-      else hcons (u,n+k)
+	(Level.set,n+k)
+      else (u,n+k)
 	
     let super (u,n as x) (v,n' as y) =
       let cmp = Level.compare u v in
@@ -401,31 +217,29 @@ struct
       let v' = f v in 
 	if v' == v then x
 	else if Level.is_prop v' && n != 0 then
-	  hcons (Level.set, n)
-	else hcons (v', n)
+	  (Level.set, n)
+	else (v', n)
 
   end
-    
-  module Huniv = HList.Make(Expr.HExpr)
-  type t = Huniv.t
-  open Huniv
-    
-  let equal x y = x == y || 
-    (Huniv.hash x == Huniv.hash y && 
-       Huniv.for_all2 Expr.equal x y)
 
-  let make l = Huniv.tip (Expr.make l)
-  let tip x = Huniv.tip x
-    
+  type t = Expr.t list
+
+  let tip u = [u]
+  let cons u v = u :: v
+
+  let equal x y = x == y || List.equal Expr.equal x y
+
+  let make l = tip (Expr.make l)
+
   let pr l = match l with
-    | Cons (u, _, Nil) -> Expr.pr u
+    | [u] -> Expr.pr u
     | _ -> 
       str "max(" ++ hov 0
-	(prlist_with_sep pr_comma Expr.pr (to_list l)) ++
+	(prlist_with_sep pr_comma Expr.pr l) ++
         str ")"
 
   let level l = match l with
-    | Cons (l, _, Nil) -> Expr.level l
+    | [l] -> Expr.level l
     | _ -> None
 
   (* The lower predicative level of the hierarchy that contains (impredicative)
@@ -445,16 +259,16 @@ struct
   (* Returns the formal universe that lies juste above the universe variable u.
      Used to type the sort u. *)
   let super l = 
-    Huniv.map (fun x -> Expr.successor x) l
+    List.map (fun x -> Expr.successor x) l
 
   let addn n l =
-    Huniv.map (fun x -> Expr.addn n x) l
+    List.map (fun x -> Expr.addn n x) l
 
   let rec merge_univs l1 l2 =
     match l1, l2 with
-    | Nil, _ -> l2
-    | _, Nil -> l1
-    | Cons (h1, _, t1), Cons (h2, _, t2) ->
+    | [], _ -> l2
+    | _, [] -> l1
+    | h1 :: t1, h2 :: t2 ->
       (match Expr.super h1 h2 with
       | Inl true (* h1 < h2 *) -> merge_univs t1 l2
       | Inl false -> merge_univs l1 t2
@@ -466,28 +280,28 @@ struct
   let sort u =
     let rec aux a l = 
       match l with
-      | Cons (b, _, l') ->
+      | b :: l' ->
         (match Expr.super a b with
 	| Inl false -> aux a l'
 	| Inl true -> l
 	| Inr c ->
 	  if c <= 0 then cons a l
 	  else cons b (aux a l'))
-      | Nil -> cons a l
+      | [] -> cons a l
     in 
-      fold (fun a acc -> aux a acc) u nil
+      List.fold_right (fun a acc -> aux a acc) u []
 	
   (* Returns the formal universe that is greater than the universes u and v.
      Used to type the products. *)
   let sup x y = merge_univs x y
 
-  let empty = nil
+  let empty = []
 
-  let exists = Huniv.exists
+  let exists = List.exists
 
-  let for_all = Huniv.for_all
+  let for_all = List.for_all
 
-  let smartmap = Huniv.smartmap
+  let smartmap = List.smartmap
 
 end
 
@@ -552,7 +366,7 @@ let repr g u =
     let a =
       try UMap.find u g
       with Not_found -> anomaly ~label:"Univ.repr"
-	  (str"Universe " ++ Level.pr u ++ str" undefined")
+	  (str"Universe " ++ Level.pr u ++ str" undefined.")
     in
     match a with
       | Equiv v -> repr_rec v
@@ -775,9 +589,9 @@ let check_equal_expr g x y =
 
 let check_eq_univs g l1 l2 =
   let f x1 x2 = check_equal_expr g x1 x2 in
-  let exists x1 l = Huniv.exists (fun x2 -> f x1 x2) l in
-    Huniv.for_all (fun x1 -> exists x1 l2) l1
-    && Huniv.for_all (fun x2 -> exists x2 l1) l2
+  let exists x1 l = List.exists (fun x2 -> f x1 x2) l in
+    List.for_all (fun x1 -> exists x1 l2) l1
+    && List.for_all (fun x2 -> exists x2 l1) l2
 
 let check_eq g u v =
   Universe.equal u v || check_eq_univs g u v
@@ -791,11 +605,11 @@ let check_smaller_expr g (u,n) (v,m) =
     | _ -> false
 
 let exists_bigger g ul l =
-  Huniv.exists (fun ul' -> 
+  Universe.exists (fun ul' -> 
     check_smaller_expr g ul ul') l
 
 let real_check_leq g u v =
-  Huniv.for_all (fun ul -> exists_bigger g ul v) u
+  Universe.for_all (fun ul -> exists_bigger g ul v) u
     
 let check_leq g u v =
   Universe.equal u v ||
@@ -855,7 +669,7 @@ let merge g arcu arcv =
       else (max_rank, old_max_rank, best_arc, arc::rest)
     in
       match between g arcu arcv with
-      | [] -> anomaly (str "Univ.between")
+      | [] -> anomaly (str "Univ.between.")
       | arc::rest ->
         let (max_rank, old_max_rank, best_arc, rest) =
           List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in
@@ -918,7 +732,7 @@ let enforce_univ_eq u v g =
       | FastLT -> error_inconsistency Eq u v
       | FastLE -> merge g arcv arcu
       | FastNLE -> merge_disc g arcu arcv
-      | FastEQ -> anomaly (Pp.str "Univ.compare"))
+      | FastEQ -> anomaly (Pp.str "Univ.compare."))
 
 (* enforce_univ_leq : Level.t -> Level.t -> unit *)
 (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
@@ -931,7 +745,7 @@ let enforce_univ_leq u v g =
     | FastLT -> error_inconsistency Le u v
     | FastLE  -> merge g arcv arcu
     | FastNLE -> fst (setleq g arcu arcv)
-    | FastEQ -> anomaly (Pp.str "Univ.compare")
+    | FastEQ -> anomaly (Pp.str "Univ.compare.")
 
 (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
 let enforce_univ_lt u v g =
@@ -944,7 +758,7 @@ let enforce_univ_lt u v g =
     | FastNLE ->
       match fast_compare_neq false g arcv arcu with
 	FastNLE -> fst (setlt g arcu arcv)
-      | FastEQ -> anomaly (Pp.str "Univ.compare")
+      | FastEQ -> anomaly (Pp.str "Univ.compare.")
       | FastLE | FastLT -> error_inconsistency Lt u v
 
 (* Prop = Set is forbidden here. *)
@@ -975,7 +789,23 @@ struct
       else Level.compare v v'
 end
 
-module Constraint = Set.Make(UConstraintOrd)
+let pr_constraint_type op = 
+  let op_str = match op with
+    | Lt -> " < "
+    | Le -> " <= "
+    | Eq -> " = "
+  in str op_str
+
+module Constraint = 
+struct 
+  module S = Set.Make(UConstraintOrd)
+  include S
+
+  let pr prl c =
+    fold (fun (u1,op,u2) pp_std ->
+      pp_std ++ prl u1 ++ pr_constraint_type op ++
+	prl u2 ++ fnl () )  c (str "")
+end
 
 let empty_constraint = Constraint.empty
 let merge_constraints c g =
@@ -990,41 +820,6 @@ type 'a constrained = 'a * constraints
 
 type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 
-let constraint_add_leq v u c =
-  (* We just discard trivial constraints like u<=u *)
-  if Expr.equal v u then c
-  else 
-    match v, u with
-    | (x,n), (y,m) -> 
-    let j = m - n in
-      if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then
-	Constraint.add (x,Lt,y) c
-      else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
-	if Level.equal x y then (* u+(k+1) <= u *)
-	  raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u))
-	else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints")
-      else if j = 0 then
-	Constraint.add (x,Le,y) c
-      else (* j >= 1 *) (* m = n + k, u <= v+k *)
-	if Level.equal x y then c (* u <= u+k, trivial *)
-	else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
-	else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints")
-	  
-let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
-
-let check_univ_leq u v = 
-  Universe.for_all (fun u -> check_univ_leq_one u v) u
-
-let enforce_leq u v c =
-  match v with
-  | Universe.Huniv.Cons (v, _, Universe.Huniv.Nil) ->
-    Universe.Huniv.fold (fun u -> constraint_add_leq u v) u c
-  | _ -> anomaly (Pp.str"A universe bound can only be a variable")
-
-let enforce_leq u v c =
-  if check_univ_leq u v then c
-  else enforce_leq u v c
-
 let check_constraint g (l,d,r) =
   match d with
   | Eq -> check_equal g l r
@@ -1046,14 +841,6 @@ type universe_level_subst = universe_level universe_map
 (** A full substitution might involve algebraic universes *)
 type universe_subst = universe universe_map
 
-let level_subst_of f = 
-  fun l -> 
-    try let u = f l in 
-	  match Universe.level u with
-	  | None -> l
-	  | Some l -> l
-    with Not_found -> l
-     
 module Instance : sig 
     type t = Level.t array
 
@@ -1062,68 +849,27 @@ module Instance : sig
     val equal : t -> t -> bool
     val subst_fn : universe_level_subst_fn -> t -> t
     val subst : universe_level_subst -> t -> t
-    val pr : t -> Pp.std_ppcmds
-    val check_eq : t check_function 
+    val pr : t -> Pp.t
+    val check_eq : t check_function
+    val length : t -> int
+    val append : t -> t -> t
+    val of_array : Level.t array -> t
 end = 
 struct
   type t = Level.t array
 
-  let empty : t = [||]
-
-  module HInstancestruct =
-  struct
-    type _t = t
-    type t = _t
-    type u = Level.t -> Level.t
-
-    let hashcons huniv a = 
-      let len = Array.length a in
-	if Int.equal len 0 then empty
-	else begin
-	  for i = 0 to len - 1 do
-	    let x = Array.unsafe_get a i in
-	    let x' = huniv x in
-	      if x == x' then ()
-	      else Array.unsafe_set a i x'
-	  done;
-	  a
-	end
-
-    let eq t1 t2 =
-      t1 == t2 ||
-	(Int.equal (Array.length t1) (Array.length t2) &&
-	   let rec aux i =
-	     (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
-	   in aux 0)
-	
-    let hash a = 
-      let accu = ref 0 in
-	for i = 0 to Array.length a - 1 do
-	  let l = Array.unsafe_get a i in
-	  let h = Level.hash l in
-	    accu := Hashset.Combine.combine !accu h;
-	done;
-	(* [h] must be positive. *)
-	let h = !accu land 0x3FFFFFFF in
-	  h
-  end
-
-  module HInstance = Hashcons.Make(HInstancestruct)
-
-  let hcons = Hashcons.simple_hcons HInstance.generate HInstance.hcons Level.hcons
-    
-  let empty = hcons [||]
+  let empty = [||]
 
   let is_empty x = Int.equal (Array.length x) 0
 
   let subst_fn fn t = 
     let t' = CArray.smartmap fn t in
-      if t' == t then t else hcons t'
+      if t' == t then t else t'
 
   let subst s t =
     let t' = 
       CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t
-    in if t' == t then t else hcons t'
+    in if t' == t then t else t'
 
   let pr =
     prvect_with_sep spc Level.pr
@@ -1142,8 +888,41 @@ struct
 	   (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1))
 	 in aux 0)
 
+  let length = Array.length
+
+  let append = Array.append
+
+  let of_array i = i
+
 end
 
+(** Substitute instance inst for ctx in csts *)
+
+let subst_instance_level s l =
+  match l.Level.data with
+  | Level.Var n -> s.(n) 
+  | _ -> l
+
+let subst_instance_instance s i = 
+  Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+  let u' = Universe.smartmap f u in
+    if u == u' then u
+    else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+  let u' = subst_instance_level s u in
+  let v' = subst_instance_level s v in
+    if u' == u && v' == v then c
+    else (u',d,v')
+
+let subst_instance_constraints s csts =
+  Constraint.fold 
+    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+    csts Constraint.empty
+
 type universe_instance = Instance.t
 
 type 'a puniverses = 'a * Instance.t
@@ -1159,10 +938,80 @@ struct
   let make x = x
   let instance (univs, cst) = univs
   let constraints (univs, cst) = cst
+  let size (univs, _) = Instance.length univs
+
+  let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
+  let pr prl (univs, cst as ctx) =
+    if is_empty ctx then mt() else
+      h 0 (Instance.pr univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 end
 
 type universe_context = UContext.t
 
+module AUContext =
+struct
+  include UContext
+
+  let repr (inst, cst) =
+    (Array.mapi (fun i l -> Level.var i) inst, cst)
+
+  let instantiate inst (u, cst) =
+    assert (Array.length u = Array.length inst);
+    subst_instance_constraints inst cst
+
+end
+
+type abstract_universe_context = AUContext.t
+
+module Variance =
+struct
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  let check_subtype x y = match x, y with
+  | (Irrelevant | Covariant | Invariant), Irrelevant -> true
+  | Irrelevant, Covariant -> false
+  | (Covariant | Invariant), Covariant -> true
+  | (Irrelevant | Covariant), Invariant -> false
+  | Invariant, Invariant -> true
+
+  let leq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant -> Constraint.add (u, Le, u') csts
+    | Invariant -> Constraint.add (u, Eq, u') csts
+
+  let eq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant | Invariant -> Constraint.add (u, Eq, u') csts
+
+  let leq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 leq_constraint csts variance u u'
+
+  let eq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 eq_constraint csts variance u u'
+end
+
+module CumulativityInfo =
+struct
+  type t = universe_context * Variance.t array
+
+  let univ_context (univcst, subtypcst) = univcst
+  let variance (univs, variance) = variance
+
+end
+
+module ACumulativityInfo = CumulativityInfo
+type abstract_cumulativity_info = ACumulativityInfo.t
+
 module ContextSet =
 struct
   type t = LSet.t constrained
@@ -1173,6 +1022,18 @@ struct
 end
 type universe_context_set = ContextSet.t
 
+(** Instance subtyping *)
+
+let check_subtype univs ctxT ctx =
+  if AUContext.size ctx == AUContext.size ctx then
+    let (inst, cst) = AUContext.repr ctx in
+    let cstT = UContext.constraints (AUContext.repr ctxT) in
+    let push accu v = add_universe v false accu in
+    let univs = Array.fold_left push univs inst in
+    let univs = merge_constraints cstT univs in
+    check_constraints cst univs
+  else false
+
 (** Substitutions. *)
 
 let is_empty_subst = LMap.is_empty
@@ -1192,43 +1053,9 @@ let subst_univs_level_universe subst u =
     if u == u' then u
     else Universe.sort u'
 
-(** Substitute instance inst for ctx in csts *)
-
-let subst_instance_level s l =
-  match l.Level.data with
-  | Level.Var n -> s.(n) 
-  | _ -> l
-
-let subst_instance_instance s i = 
-  Array.smartmap (fun l -> subst_instance_level s l) i
-
-let subst_instance_universe s u =
-  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-  let u' = Universe.smartmap f u in
-    if u == u' then u
-    else Universe.sort u'
-
-let subst_instance_constraint s (u,d,v as c) =
-  let u' = subst_instance_level s u in
-  let v' = subst_instance_level s v in
-    if u' == u && v' == v then c
-    else (u',d,v')
-
-let subst_instance_constraints s csts =
-  Constraint.fold 
-    (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)
-
-let instantiate_univ_constraints u (_, csts) = 
-  subst_instance_constraints u csts
-
 (** With level to universe substitutions. *)
 type universe_subst_fn = universe_level -> universe
 
@@ -1239,7 +1066,7 @@ let subst_univs_expr_opt fn (l,n) =
 
 let subst_univs_universe fn ul =
   let subst, nosubst = 
-    Universe.Huniv.fold (fun u (subst,nosubst) -> 
+    List.fold_right (fun u (subst,nosubst) -> 
       try let a' = subst_univs_expr_opt fn u in
 	    (a' :: subst, nosubst)
       with Not_found -> (subst, u :: nosubst))
@@ -1250,7 +1077,7 @@ let subst_univs_universe fn ul =
       let substs = 
 	List.fold_left Universe.merge_univs Universe.empty subst
       in
-	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u))
+	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u))
 	  substs nosubst
 
 let merge_context strict ctx g =
@@ -1269,6 +1096,10 @@ let merge_context_set strict ctx g =
 
 (** Pretty-printing *)
 
+let pr_constraints prl = Constraint.pr prl
+    
+let pr_universe_context = UContext.pr
+
 let pr_arc = function
   | _, Canonical {univ=u; lt=[]; le=[]} ->
       mt ()
diff --git a/checker/univ.mli b/checker/univ.mli
index 7d4c629a..473159c0 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Universes. *)
@@ -18,6 +20,11 @@ sig
   (** Create a new universe level from a unique identifier and an associated
       module path. *)
 
+  val var : int -> t
+
+  val pr : t -> Pp.t
+  (** Pretty-printing *)
+  
   val equal : t -> t -> bool
 end
 
@@ -48,7 +55,7 @@ type universe = Universe.t
 
 (** Alias name. *)
 
-val pr_uni : universe -> Pp.std_ppcmds
+val pr_uni : universe -> Pp.t
 
 (** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ...
    Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
@@ -71,11 +78,13 @@ type 'a check_function = universes -> 'a -> 'a -> bool
 val check_leq : universe check_function
 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. *)
+   @raise AlreadyDeclared if the level is already declared in the graph. *)
 
 exception AlreadyDeclared
 
@@ -99,8 +108,6 @@ type 'a constrained = 'a * constraints
 
 type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 
-val enforce_leq : universe constraint_function
-
 (** {6 ... } *)
 (** Merge of constraints in a universes graph.
   The function [merge_constraints] merges a set of constraints in a given
@@ -143,8 +150,6 @@ type universe_level_subst_fn = universe_level -> universe_level
 type universe_subst = universe universe_map
 type universe_level_subst = universe_level universe_map
 
-val level_subst_of : universe_subst_fn -> universe_level_subst_fn
-
 (** {6 Universe instances} *)
 
 module Instance :
@@ -157,7 +162,6 @@ sig
   val is_empty : t -> bool
 
   val equal : t -> t -> bool
-  (** Equality (note: instances are hash-consed, this is O(1)) *)
 
   val subst_fn : universe_level_subst_fn -> t -> t
   (** Substitution by a level-to-level function. *)
@@ -165,11 +169,19 @@ sig
   val subst : universe_level_subst -> t -> t
   (** Substitution by a level-to-level function. *)
 
-  val pr : t -> Pp.std_ppcmds
+  val pr : t -> Pp.t
   (** Pretty-printing, no comments *)
 
   val check_eq : t check_function
   (** Check equality of instances w.r.t. a universe graph *)
+
+  val length : t -> int
+  (** Compute the length of the instance  *)
+
+  val of_array : Level.t array -> t
+
+  val append : t -> t -> t
+  (** Append two universe instances *)
 end
 
 type universe_instance = Instance.t
@@ -187,9 +199,49 @@ sig
   val make : universe_instance constrained -> t
   val instance : t -> Instance.t
   val constraints : t -> constraints
+  val is_empty : t -> bool
+    
+end
+
+type universe_context = UContext.t
+
+module AUContext :
+sig
+  type t
+
+  val size : t -> int
+
+  val instantiate : Instance.t -> t -> Constraint.t
+  val repr : t -> UContext.t
 
 end
 
+type abstract_universe_context = AUContext.t
+
+module Variance :
+sig
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+  val check_subtype : t -> t -> bool
+  val leq_constraints : t array -> Instance.t constraint_function
+  val eq_constraints : t array -> Instance.t constraint_function
+end
+
+
+module ACumulativityInfo :
+sig
+  type t
+
+  val univ_context : t -> abstract_universe_context
+  val variance : t -> Variance.t array
+
+end
+
+type abstract_cumulativity_info = ACumulativityInfo.t
+
 module ContextSet :
   sig 
     type t
@@ -198,7 +250,6 @@ module ContextSet :
     val constraints : t -> constraints
   end
 
-type universe_context = UContext.t
 type universe_context_set = ContextSet.t
 
 val merge_context : bool -> universe_context -> universes -> universes
@@ -221,18 +272,20 @@ val subst_univs_universe : universe_subst_fn -> universe -> universe
 (** Substitution of instances *)
 val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
 val subst_instance_universe : universe_instance -> universe -> universe
-val subst_instance_constraints : universe_instance -> constraints -> constraints
 
 (* val make_instance_subst : universe_instance -> universe_level_subst *)
 (* val make_inverse_instance_subst : universe_instance -> universe_level_subst *)
 
-(** Get the instantiated graph. *)
-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
-									    
+val make_abstract_instance : abstract_universe_context -> universe_instance
+
+(** Check instance subtyping *)
+val check_subtype : universes -> AUContext.t -> AUContext.t -> bool
+
 (** {6 Pretty-printing of universes. } *)
 
-val pr_universes : universes -> Pp.std_ppcmds
+val pr_constraint_type : constraint_type -> Pp.t
+val pr_constraints : (Level.t -> Pp.t) -> constraints -> Pp.t
+val pr_universe_context : (Level.t -> Pp.t) -> universe_context -> Pp.t
+
+val pr_universes : universes -> Pp.t
diff --git a/checker/validate.ml b/checker/validate.ml
index c434ef09..f831875d 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* This module defines validation functions to ensure an imported
@@ -49,8 +51,6 @@ let (/) (ctx:error_context) s : error_context = s::ctx
 exception ValidObjError of string * error_context * Obj.t
 let fail ctx o s = raise (ValidObjError(s,ctx,o))
 
-type func = error_context -> Obj.t -> unit
-
 (* Check that object o is a block with tag t *)
 let val_tag t ctx o =
   if Obj.is_block o && Obj.tag o = t then ()
diff --git a/checker/validate.mli b/checker/validate.mli
new file mode 100644
index 00000000..6c2ab8d3
--- /dev/null
+++ b/checker/validate.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val validate : bool -> Values.value -> 'a -> unit
diff --git a/checker/values.ml b/checker/values.ml
index c175aed6..1ac8d7ce 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Abstract representations of values in a vo *)
@@ -13,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 6466d8cc443b5896cb905776df0cc49e  checker/cic.mli
+MD5 c4fdf8a846aed45c27b5acb1add7d1c6 checker/cic.mli
 
 *)
 
@@ -54,6 +56,7 @@ let v_enum name n = Sum(name,n,[||])
 
 let v_pair v1 v2 = v_tuple "*" [|v1; v2|]
 let v_bool = v_enum "bool" 2
+let v_unit = v_enum "unit" 1
 let v_ref v = v_tuple "ref" [|v|]
 
 let v_set v =
@@ -69,6 +72,8 @@ let v_map vk vd =
 let v_hset v = v_map Int (v_set v)
 let v_hmap vk vd = v_map Int (v_map vk vd)
 
+let v_pred v = v_pair v_bool (v_set v)
+
 (* lib/future *)
 let v_computation f =
   Annot ("Future.computation",
@@ -98,7 +103,7 @@ let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *)
   [|(*Level*)[|Int;v_dp|]; (*Var*)[|Int|]|]
 let v_level = v_tuple "level" [|Int;v_raw_level|] 
 let v_expr = v_tuple "levelexpr" [|v_level;Int|]
-let rec v_univ = Sum ("universe", 1, [| [|v_expr; Int; v_univ|] |])
+let v_univ = List v_expr
 
 let v_cstrs =
   Annot
@@ -107,8 +112,12 @@ let v_cstrs =
        (v_tuple "univ_constraint"
           [|v_level;v_enum "order_request" 3;v_level|]))
 
+let v_variance = v_enum "variance" 3
+
 let v_instance = Annot ("instance", Array v_level)
 let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|]
+let v_abs_context = v_context (* only for clarity *)
+let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|]
 let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
 (** kernel/term *)
@@ -196,12 +205,20 @@ let v_lazy_constr =
 let v_impredicative_set = v_enum "impr-set" 2
 let v_engagement = v_impredicative_set
 
+let v_conv_level =
+  v_sum "conv_level" 2 [|[|Int|]|]
+
+let v_oracle =
+  v_tuple "oracle" [|
+    v_map v_id v_conv_level;
+    v_hmap v_cst v_conv_level;
+    v_pred v_id;
+    v_pred v_cst;
+  |]
+
 let v_pol_arity =
   v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
 
-let v_cst_type =
-  v_sum "constant_type" 0 [|[|v_constr|]; [|v_pair v_rctxt v_pol_arity|]|]
-
 let v_cst_def =
   v_sum "constant_def" 0
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
@@ -213,15 +230,16 @@ let v_projbody =
 	    v_constr|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool; v_bool|]
+  v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
+
+let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
     v_cst_def;
-    v_cst_type;
+    v_constr;
     Any;
-    v_bool;
-    v_context;
+    v_const_univs;
     Opt v_projbody;
     v_bool;
     v_typing_flags|]
@@ -262,6 +280,10 @@ let v_finite = v_enum "recursivity_kind" 3
 let v_mind_record = Annot ("mind_record", 
 			   Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |])))
 
+let v_ind_pack_univs = 
+  v_sum "abstract_inductive_universes" 0
+    [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|]
+
 let v_ind_pack = v_tuple "mutual_inductive_body"
   [|Array v_one_ind;
     v_mind_record;
@@ -271,21 +293,15 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Int;
     Int;
     v_rctxt;
-    v_bool;
-    v_context;
+    v_ind_pack_univs; (* universes *)
     Opt v_bool;
     v_typing_flags|]
 
-let v_with =
-  Sum ("with_declaration_body",0,
-       [|[|List v_id;v_mp|];
-         [|List v_id;v_tuple "with_def" [|v_constr;v_context|]|]|])
-
 let rec v_mae =
   Sum ("module_alg_expr",0,
   [|[|v_mp|];         (* SEBident *)
     [|v_mae;v_mp|];   (* SEBapply *)
-    [|v_mae;v_with|]  (* SEBwith *)
+    [|v_mae; Any|]  (* SEBwith *)
   |])
 
 let rec v_sfb =
@@ -308,13 +324,13 @@ and v_impl =
   Sum ("module_impl",2, (* Abstract, FullStruct *)
   [|[|v_mexpr|];  (* Algebraic *)
     [|v_sign|]|])  (* Struct *)
-and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *)
+and v_noimpl = v_unit
 and v_module =
   Tuple ("module_body",
          [|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_context_set;v_resolver;Any|])
+         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|])
 
 (** kernel/safe_typing *)
 
@@ -368,22 +384,3 @@ let v_lib =
 let v_opaques = Array (v_computation v_constr)
 let v_univopaques =
   Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|]))
-
-(** Registering dynamic values *)
-
-module IntOrd =
-struct
-  type t = int
-  let compare (x : t) (y : t) = compare x y
-end
-
-module IntMap = Map.Make(IntOrd)
-
-let dyn_table : value IntMap.t ref = ref IntMap.empty
-
-let register_dyn name t =
-  dyn_table := IntMap.add name t !dyn_table
-
-let find_dyn name =
-  try IntMap.find name !dyn_table
-  with Not_found -> Any
diff --git a/checker/values.mli b/checker/values.mli
new file mode 100644
index 00000000..20b9d54a
--- /dev/null
+++ b/checker/values.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type value =
+  | Any
+  | Fail of string
+  | Tuple of string * value array
+  | Sum of string * int * value array array
+  | Array of value
+  | List of value
+  | Opt of value
+  | Int
+  | String
+  | Annot of string * value
+  | Dyn
+
+val v_univopaques : value
+val v_libsum : value
+val v_lib : value
+val v_opaques : value
+val v_stm_seg : value
diff --git a/checker/votour.ml b/checker/votour.ml
index 48f9f45e..bc820e23 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -1,15 +1,19 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Values
 
 (** {6 Interactive visit of a vo} *)
 
+let max_string_length = 1024
+
 let rec read_num max =
   let quit () =
     Printf.printf "\nGoodbye!\n%!";
@@ -19,14 +23,14 @@ let rec read_num max =
   if l = "u" then None
   else if l = "x" then quit ()
   else
-    try
-      let v = int_of_string l in
+    match int_of_string l with
+    | v ->
       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" ->
+    | exception Failure _ ->
       Printf.printf "Unrecognized input! <n> enters the <n>-th child, u goes up 1 level, x exits\n%!";
       read_num max
 
@@ -75,48 +79,51 @@ struct
 
   type obj = data
 
-  let memory = ref [||]
-  let sizes = ref [||]
+  let memory = ref LargeArray.empty
+  let sizes = ref LargeArray.empty
   (** size, in words *)
 
   let ws = Sys.word_size / 8
 
-  let rec init_size seen = function
-  | Int _ | Atm _ | Fun _ -> 0
+  let rec init_size seen k = function
+  | Int _ | Atm _ | Fun _ -> k 0
   | Ptr p ->
-    if seen.(p) then 0
+    if LargeArray.get seen p then k 0
     else
-      let () = seen.(p) <- true in
-      match (!memory).(p) with
+      let () = LargeArray.set seen p true in
+      match LargeArray.get !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
+        let len = Array.length os in
+        let rec fold i accu k =
+          if i == len then k accu
+          else
+            init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i)
+        in
+        fold 0 1 (fun size -> let () = LargeArray.set !sizes p size in k size)
       | String s ->
         let size = 2 + (String.length s / ws) in
-        let () = (!sizes).(p) <- size in
-        size
+        let () = LargeArray.set !sizes p size in
+        k size
 
   let size = function
   | Int _ | Atm _ | Fun _ -> 0
-  | Ptr p -> (!sizes).(p)
+  | Ptr p -> LargeArray.get !sizes p
 
   let repr = function
   | Int i -> INT i
   | Atm t -> BLOCK (t, [||])
   | Fun _ -> OTHER
   | Ptr p ->
-    match (!memory).(p) with
+    match LargeArray.get !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
+    let () = sizes := LargeArray.make (LargeArray.length mem) (-1) in
+    let seen = LargeArray.make (LargeArray.length mem) false in
+    let () = init_size seen ignore obj in
     obj
 
   let oid = function
@@ -149,22 +156,25 @@ let rec get_name ?(extra=false) = function
 (** For tuples, its quite handy to display the inner 1st string (if any).
     Cf. [structure_body] for instance *)
 
+exception TupleString of string
 let get_string_in_tuple o =
   try
     for i = 0 to Array.length o - 1 do
       match Repr.repr o.(i) with
       | STRING s ->
-        failwith (Printf.sprintf " [..%s..]" s)
+        let len = min max_string_length (String.length s) in
+        raise (TupleString (Printf.sprintf " [..%s..]" (String.sub s 0 len)))
       | _ -> ()
     done;
     ""
-  with Failure s -> s
+  with TupleString s -> s
 
 (** Some details : tags, integer value for non-block, etc etc *)
 
 let rec get_details v o = match v, Repr.repr o with
   | (String | Any), STRING s ->
-    Printf.sprintf " [%s]" (String.escaped s)
+    let len = min max_string_length (String.length s) in
+    Printf.sprintf " [%s]" (String.escaped (String.sub s 0 len))
   |Tuple (_,v), BLOCK (_, o) -> get_string_in_tuple o
   |(Sum _|Any), BLOCK (tag, _) ->
     Printf.sprintf " [tag=%i]" tag
@@ -191,20 +201,20 @@ let access_children vs os pos =
   else raise Exit
 
 let access_list v o pos =
-  let rec loop o pos = match Repr.repr o with
-  | INT 0 -> []
+  let rec loop o pos accu = match Repr.repr o with
+  | INT 0 -> List.rev accu
   | BLOCK (0, [|hd; tl|]) ->
-    (v, hd, 0 :: pos) :: loop tl (1 :: pos)
+    loop tl (1 :: pos) ((v, hd, 0 :: pos) :: accu)
   | _ -> raise Exit
   in
-  Array.of_list (loop o pos)
+  Array.of_list (loop o pos [])
 
 let access_block o = match Repr.repr o with
 | BLOCK (tag, os) -> (tag, os)
 | _ -> raise Exit
-let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit
 
 (** raises Exit if the object has not the expected structure *)
+exception Forbidden
 let rec get_children v o pos = match v with
   |Tuple (_, v) ->
     let (_, os) = access_block o in
@@ -225,18 +235,26 @@ let rec get_children v o pos = match v with
     | BLOCK (0, [|x|]) -> [|(v, x, 0 :: pos)|]
     | _ -> raise Exit
     end
-  |String | Int -> [||]
+  | String ->
+    begin match Repr.repr o with
+    | STRING _ -> [||]
+    | _ -> raise Exit
+    end
+  | Int ->
+    begin match Repr.repr o with
+    | INT _ -> [||]
+    | _ -> raise Exit
+    end
   |Annot (s,v) -> get_children v o pos
   |Any -> raise Exit
   |Dyn ->
     begin match Repr.repr o with
     | BLOCK (0, [|id; o|]) ->
-      let n = access_int id in
-      let tpe = find_dyn n in
+      let tpe = Any in
       [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|]
     | _ -> raise Exit
     end
-  |Fail s -> failwith "forbidden"
+  |Fail s -> raise Forbidden
 
 let get_children v o pos =
   try get_children v o pos
@@ -257,9 +275,10 @@ let init () = stk := []
 
 let push name v o p = stk := { nam = name; typ = v; obj = o; pos = p } :: !stk
 
+exception EmptyStack
 let pop () = match !stk with
   | i::s -> stk := s; i
-  | _ -> failwith "empty stack"
+  | _ -> raise EmptyStack
 
 let rec visit v o pos =
   Printf.printf "\nDepth %d Pos %s Context %s\n"
@@ -283,8 +302,8 @@ let rec visit v o pos =
        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
+  | EmptyStack -> ()
+  | Forbidden -> let info = pop () in visit info.typ info.obj info.pos
   | Failure _ | Invalid_argument _ -> visit v o pos
 
 end
@@ -313,8 +332,7 @@ let dummy_header = {
 }
 
 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 magic = really_input_string chan 4 in
   let length = input_binary_int chan in
   let objects = input_binary_int chan in
   let size32 = input_binary_int chan in
@@ -377,7 +395,7 @@ let visit_vo f =
     | None -> ()
   done
 
-let main =
+let () =
   if not !Sys.interactive then
     Arg.parse [] visit_vo
       ("votour: guided tour of a Coq .vo or .vi file\n"^
diff --git a/checker/votour.mli b/checker/votour.mli
new file mode 100644
index 00000000..9db9ecd1
--- /dev/null
+++ b/checker/votour.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+   that does not have a corresponding .mli file *)