Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

38 files changed, 288 insertions, 225 deletions

diff --git a/checker/check.ml b/checker/check.ml
index c835cec824..3a5c91217d 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -46,7 +46,7 @@ type library_t = {
   library_opaques : Cic.opaque_table;
   library_deps : Cic.library_deps;
   library_digest : Cic.vodigest;
-  library_extra_univs : Univ.constraints }
+  library_extra_univs : Univ.ContextSet.t }
 
 module LibraryOrdered =
   struct
@@ -97,7 +97,7 @@ let access_opaque_univ_table dp i =
     let t = LibraryMap.find dp !opaque_univ_tables in
     assert (i < Array.length t);
     Future.force t.(i)
-  with Not_found -> Univ.empty_constraint
+  with Not_found -> Univ.ContextSet.empty
 
 
 let _ = Declarations.indirect_opaque_access := access_opaque_table
@@ -271,20 +271,10 @@ let try_locate_qualified_library qid =
     | LibNotFound -> error_lib_not_found qid
 
 (************************************************************************)
-(*s Low-level interning/externing of libraries to files *)
+(*s Low-level interning of libraries from files *)
 
-(*s Loading from disk to cache (preparation phase) *)
-
-let raw_intern_library =
-  snd (System.raw_extern_intern Coq_config.vo_magic_number)
-
-let with_magic_number_check f a =
-  try f a
-  with System.Bad_magic_number fname ->
-    errorlabstrm "with_magic_number_check"
-    (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++
-    spc () ++ str"It is corrupted" ++ spc () ++
-    str"or was compiled with another version of Coq.")
+let raw_intern_library f =
+  System.raw_intern_state Coq_config.vo_magic_number f
 
 (************************************************************************)
 (* Internalise libraries *)
@@ -312,7 +302,7 @@ let intern_from_file (dir, f) =
   Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
   let (sd,md,table,opaque_csts,digest) =
     try
-      let ch = with_magic_number_check raw_intern_library f in
+      let ch = System.with_magic_number_check raw_intern_library f in
       let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in
       let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in
       let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in
@@ -357,9 +347,8 @@ let intern_from_file (dir, f) =
       LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables)
     opaque_csts;
   let extra_cst =
-    Option.default Univ.empty_constraint
-      (Option.map (fun (_,cs,_) ->
-         Univ.ContextSet.constraints cs) opaque_csts) in
+    Option.default Univ.ContextSet.empty
+      (Option.map (fun (_,cs,_) -> cs) opaque_csts) in
   mk_library sd md f table digest extra_cst
 
 let get_deps (dir, f) =
diff --git a/checker/check.mllib b/checker/check.mllib
index 246fe64dee..900cfe0c82 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -8,6 +8,7 @@ Hashcons
 CSet
 CMap
 Int
+Dyn
 HMap
 Option
 Store
@@ -17,6 +18,8 @@ Flags
 Control
 Pp_control
 Loc
+CList
+CString
 Serialize
 Stateid
 Feedback
@@ -25,14 +28,12 @@ Segmenttree
 Unicodetable
 Unicode
 CObj
-CList
-CString
 CArray
 CStack
 Util
 Ppstyle
 Errors
-Ephemeron
+CEphemeron
 Future
 CUnix
 
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index d041f1b7e1..d031975d79 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/check_stat.mli b/checker/check_stat.mli
index 10908f0cc3..39e19d10e4 100644
--- a/checker/check_stat.mli
+++ b/checker/check_stat.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/checker.ml b/checker/checker.ml
index d5d9b9e3b8..91a207a60c 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -217,12 +217,6 @@ open Type_errors
 let anomaly_string () = str "Anomaly: "
 let report () = (str "." ++ spc () ++ str "Please report.")
 
-let print_loc loc =
-  if loc = Loc.ghost then
-    (str"<unknown>")
-  else
-    let loc = Loc.unloc loc in
-    (int (fst loc) ++ str"-" ++ int (snd loc))
 let guill s = str "\"" ++ str s ++ str "\""
 
 let where s =
@@ -337,8 +331,6 @@ let parse_args argv =
     | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
 
-    | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem
-    | "-R" :: d :: "-as" :: [] -> usage ()
     | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem
     | "-R" :: ([] | [_]) -> usage ()
 
diff --git a/checker/cic.mli b/checker/cic.mli
index 881d3ca797..00ac2f56c3 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -111,7 +111,8 @@ type cofixpoint = constr pcofixpoint
 
 (** {6 Type of assumptions and contexts}  *)
 
-type rel_declaration = Name.t * constr option * constr
+type rel_declaration = LocalAssum of Name.t * constr          (* name, type *)
+                     | LocalDef of Name.t * constr * constr   (* name, value, type *)
 type rel_context = rel_declaration list
 
 (** The declarations below in .vo should be outside sections,
@@ -380,7 +381,7 @@ and module_body =
     (** algebraic type, kept if it's relevant for extraction *)
     mod_type_alg : module_expression option;
     (** set of all constraints in the module  *)
-    mod_constraints : Univ.constraints;
+    mod_constraints : Univ.ContextSet.t;
     (** quotiented set of equivalent constants and inductive names *)
     mod_delta : delta_resolver;
     mod_retroknowledge : action list }
diff --git a/checker/closure.ml b/checker/closure.ml
index c6cc2185d3..c2708e97d2 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -217,10 +217,10 @@ let ref_value_cache info ref =
 let defined_rels flags env =
 (*  if red_local_const (snd flags) then*)
   fold_rel_context
-      (fun (id,b,t) (i,subs) ->
-	 match b with
-	   | None -> (i+1, subs)
-	   | Some body -> (i+1, (i,body) :: subs))
+      (fun decl (i,subs) ->
+	 match decl with
+	   | LocalAssum _ -> (i+1, subs)
+	   | LocalDef (_,body,_) -> (i+1, (i,body) :: subs))
       (rel_context env) ~init:(0,[])
 (*  else (0,[])*)
 
diff --git a/checker/closure.mli b/checker/closure.mli
index 376e9fef7d..8b1f246c28 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 36e6a7caba..3ce3125337 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -426,7 +426,7 @@ let subst_lazy_constr sub = function
 let indirect_opaque_access =
   ref ((fun dp i -> assert false) : DirPath.t -> int -> constr)
 let indirect_opaque_univ_access =
-  ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.constraints)
+  ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.ContextSet.t)
 
 let force_lazy_constr = function
   | Indirect (l,dp,i) ->
@@ -435,7 +435,7 @@ let force_lazy_constr = function
 
 let force_lazy_constr_univs = function
   | OpaqueDef (Indirect (l,dp,i)) -> !indirect_opaque_univ_access dp i
-  | _ -> Univ.empty_constraint
+  | _ -> Univ.ContextSet.empty
 
 let subst_constant_def sub = function
   | Undef inl -> Undef inl
@@ -457,6 +457,8 @@ let is_opaque cb = match cb.const_body with
   | OpaqueDef _ -> true
   | Def _ | Undef _ -> false
 
+let opaque_univ_context cb = force_lazy_constr_univs cb.const_body
+
 let subst_rel_declaration sub (id,copt,t as x) =
   let copt' = Option.smartmap (subst_mps sub) copt in
   let t' = subst_mps sub t in
@@ -515,11 +517,8 @@ let map_decl_arity f g = function
   | RegularArity a -> RegularArity (f a)
   | TemplateArity a -> TemplateArity (g a)
 
-
-let subst_rel_declaration sub (id,copt,t as x) =
-  let copt' = Option.smartmap (subst_mps sub) copt in
-  let t' = subst_mps sub t in
-  if copt == copt' && t == t' then x else (id,copt',t')
+let subst_rel_declaration sub =
+  Term.map_rel_decl (subst_mps sub)
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 3c6db6ab71..456df83699 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -2,17 +2,18 @@ open Names
 open Cic
 
 val force_constr : constr_substituted -> constr
-val force_lazy_constr_univs : Cic.constant_def -> Univ.constraints
+val force_lazy_constr_univs : Cic.constant_def -> Univ.ContextSet.t
 val from_val : constr -> constr_substituted
 
 val indirect_opaque_access : (DirPath.t -> int -> constr) ref
-val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.constraints) ref
+val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.ContextSet.t) ref
 
 (** Constant_body *)
 
 val body_of_constant : constant_body -> constr option
 val constant_has_body : constant_body -> bool
 val is_opaque : constant_body -> bool
+val opaque_univ_context : constant_body -> Univ.ContextSet.t
 
 (* Mutual inductives *)
 
diff --git a/checker/environ.ml b/checker/environ.ml
index 6dbc44d6b8..7040fdda46 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -80,17 +80,24 @@ let push_rel d env =
 let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x
 
 let push_rec_types (lna,typarray,_) env =
-  let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
+  let ctxt = Array.map2_i (fun i na t -> LocalAssum (na, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
 (* Universe constraints *)
-let add_constraints c env =
-  if c == Univ.Constraint.empty then
-    env
-  else
-    let s = env.env_stratification in
+let map_universes f env =
+  let s = env.env_stratification in
     { env with env_stratification =
-      { s with env_universes = Univ.merge_constraints c s.env_universes } }
+	 { s with env_universes = f s.env_universes } }
+
+let add_constraints c env =
+  if c == Univ.Constraint.empty then env
+  else map_universes (Univ.merge_constraints c) env
+			   
+let push_context ?(strict=false) ctx env =
+  map_universes (Univ.merge_context strict ctx) env
+
+let push_context_set ?(strict=false) ctx env =
+  map_universes (Univ.merge_context_set strict ctx) env
 
 let check_constraints cst env =
   Univ.check_constraints cst env.env_stratification.env_universes
diff --git a/checker/environ.mli b/checker/environ.mli
index f3b2dd839a..87f143d1bb 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -39,6 +39,8 @@ val push_rec_types : name array * constr array * 'a -> env -> env
 (* Universes *)
 val universes : env -> Univ.universes
 val add_constraints : Univ.constraints -> env -> env
+val push_context : ?strict:bool -> Univ.universe_context -> env -> env
+val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
 val check_constraints : Univ.constraints -> env -> bool
 
 (* Constants *)
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index f02f03dcb1..566df673c1 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -56,10 +56,10 @@ let is_constructor_head t =
 let conv_ctxt_prefix env (ctx1:rel_context) ctx2 =
   let rec chk env rctx1 rctx2 =
     match rctx1, rctx2 with
-        (_,None,ty1 as d1)::rctx1', (_,None,ty2)::rctx2' ->
+        (LocalAssum (_,ty1) as d1)::rctx1', LocalAssum (_,ty2)::rctx2' ->
           conv env ty1 ty2;
           chk (push_rel d1 env) rctx1' rctx2'
-      | (_,Some bd1,ty1 as d1)::rctx1', (_,Some bd2,ty2)::rctx2' ->
+      | (LocalDef (_,bd1,ty1) as d1)::rctx1', LocalDef (_,bd2,ty2)::rctx2' ->
           conv env ty1 ty2;
           conv env bd1 bd2;
           chk (push_rel d1 env) rctx1' rctx2'
@@ -94,10 +94,10 @@ let rec sorts_of_constr_args env t =
   match t with
     | Prod (name,c1,c2) ->
         let varj = infer_type env c1 in
-	let env1 = push_rel (name,None,c1) env in
+	let env1 = push_rel (LocalAssum (name,c1)) env in
 	varj :: sorts_of_constr_args env1 c2
     | LetIn (name,def,ty,c) ->
-        let env1 = push_rel (name,Some def,ty) env in
+        let env1 = push_rel (LocalDef (name,def,ty)) env in
 	sorts_of_constr_args env1 c
     | _ when is_constructor_head t -> []
     | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor")
@@ -167,7 +167,7 @@ let typecheck_arity env params inds =
 	   full_arity is used as argument or subject to cast, an
 	   upper universe will be generated *)
 	let id = ind.mind_typename in
-	let env_ar' = push_rel (Name id, None, arity) env_ar in
+	let env_ar' = push_rel (LocalAssum (Name id, arity)) env_ar in
         env_ar')
       env
       inds in
@@ -319,7 +319,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
   let nhyps = List.length hyps in
   let rec check k index = function
     | [] -> ()
-    | (_,Some _,_)::hyps -> check k (index+1) hyps
+    | LocalDef _ :: hyps -> check k (index+1) hyps
     | _::hyps ->
         match whd_betadeltaiota env lpar.(k) with
 	  | Rel w when w = index -> check (k-1) (index+1) hyps
@@ -340,7 +340,7 @@ let check_rec_par (env,n,_,_) hyps nrecp largs =
       | ([],_) -> ()
       | (_,[]) ->
           failwith "number of recursive parameters cannot be greater than the number of parameters."
-      | (lp,(_,Some _,_)::hyps) -> find (index-1) (lp,hyps)
+      | (lp,LocalDef _ :: hyps) -> find (index-1) (lp,hyps)
       | (p::lp,_::hyps) ->
           (match whd_betadeltaiota env p with
 	    | Rel w when w = index -> find (index-1) (lp,hyps)
@@ -370,14 +370,15 @@ let abstract_mind_lc env ntyps npars lc =
    [lra] is the list of recursive tree of each variable
  *)
 let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
- (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra)
+ (push_rel (LocalAssum (x,a)) env, n+1, ntypes, (Norec,ra)::lra)
 
 let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) =
   let auxntyp = 1 in
   let specif = lookup_mind_specif env mi in
   let env' =
-    push_rel (Anonymous,None,
-              hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) env in
+    let decl = LocalAssum (Anonymous,
+                           hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) in
+    push_rel decl env in
   let ra_env' =
     (Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
diff --git a/checker/indtypes.mli b/checker/indtypes.mli
index 5188f80d13..071eecbbcd 100644
--- a/checker/indtypes.mli
+++ b/checker/indtypes.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 21b80f323e..43a32ea24d 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -88,10 +88,10 @@ let instantiate_params full t u args sign =
     anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
   let (rem_args, subs, ty) =
     fold_rel_context
-      (fun (_,copt,_) (largs,subs,ty) ->
-        match (copt, largs, ty) with
-          | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
-          | (Some b,_,LetIn(_,_,_,t))    -> 
+      (fun decl (largs,subs,ty) ->
+        match (decl, largs, ty) with
+          | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t)
+          | (LocalDef (_,b,_),_,LetIn(_,_,_,t))    ->
 	    (largs, (substl subs (subst_instance_constr u b))::subs, t)
 	  | (_,[],_)                -> if full then fail() else ([], subs, ty)
 	  | _                       -> fail ())
@@ -161,7 +161,7 @@ let remember_subst u subst =
 (* Propagate the new levels in the signature *)
 let rec make_subst env =
   let rec make subst = function
-    | (_,Some _,_)::sign, exp, args ->
+    | LocalDef _ :: sign, exp, args ->
         make subst (sign, exp, args)
     | d::sign, None::exp, args ->
         let args = match args with _::args -> args | [] -> [] in
@@ -174,7 +174,7 @@ let rec make_subst env =
         (* a useless extra constraint *)
         let s = sort_as_univ (snd (dest_arity env a)) in
         make (cons_subst u s subst) (sign, exp, args)
-    | (na,None,t)::sign, Some u::exp, [] ->
+    | LocalAssum (na,t) :: sign, Some u::exp, [] ->
         (* No more argument here: we add the remaining universes to the *)
         (* substitution (when [u] is distinct from all other universes in the *)
         (* template, it is identity substitution  otherwise (ie. when u is *)
@@ -319,8 +319,8 @@ let elim_sorts (_,mip) = mip.mind_kelim
 
 let extended_rel_list n hyps =
   let rec reln l p = function
-    | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
-    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
+    | LocalDef _ :: hyps -> reln l (p+1) hyps
     | [] -> l
   in
   reln [] 1 hyps
@@ -345,12 +345,12 @@ let is_correct_arity env c (p,pj) ind specif params =
   let rec srec env pt ar =
     let pt' = whd_betadeltaiota env pt in
     match pt', ar with
-      | Prod (na1,a1,t), (_,None,a1')::ar' ->
+      | Prod (na1,a1,t), LocalAssum (_,a1')::ar' ->
           (try conv env a1 a1'
           with NotConvertible -> raise (LocalArity None));
-          srec (push_rel (na1,None,a1) env) t ar'
+          srec (push_rel (LocalAssum (na1,a1)) env) t ar'
       | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
-	 let env' = push_rel (na1,None,a1) env in
+	 let env' = push_rel (LocalAssum (na1,a1)) env in
      let ksort = match (whd_betadeltaiota env' a2) with
         | Sort s -> family_of_sort s
 	    | _ -> raise (LocalArity None) in
@@ -362,8 +362,8 @@ let is_correct_arity env c (p,pj) ind specif params =
       | Sort s', [] ->
 	  check_allowed_sort (family_of_sort s') specif;
 	  false
-      | _, (_,Some _,_ as d)::ar' ->
-	 srec (push_rel d env) (lift 1 pt') ar'
+      | _, (LocalDef _ as d)::ar' ->
+         srec (push_rel d env) (lift 1 pt') ar'
       | _ ->
 	  raise (LocalArity None)
   in
@@ -527,10 +527,10 @@ type guard_env =
 let make_renv env recarg tree =
   { env = env;
     rel_min = recarg+2; (* recarg = 0 ==> Rel 1 -> recarg; Rel 2 -> fix *)
-    genv = [Lazy.lazy_from_val(Subterm(Large,tree))] }
+    genv = [Lazy.from_val(Subterm(Large,tree))] }
 
 let push_var renv (x,ty,spec) =
-  { env = push_rel (x,None,ty) renv.env;
+  { env = push_rel (LocalAssum (x,ty)) renv.env;
     rel_min = renv.rel_min+1;
     genv = spec:: renv.genv }
 
@@ -538,7 +538,7 @@ let assign_var_spec renv (i,spec) =
   { renv with genv = List.assign renv.genv (i-1) spec }
 
 let push_var_renv renv (x,ty) =
-  push_var renv (x,ty,Lazy.lazy_from_val Not_subterm)
+  push_var renv (x,ty,Lazy.from_val Not_subterm)
 
 (* Fetch recursive information about a variable p *)
 let subterm_var p renv =
@@ -549,13 +549,13 @@ let push_ctxt_renv renv ctxt =
   let n = rel_context_length ctxt in
   { env = push_rel_context ctxt renv.env;
     rel_min = renv.rel_min+n;
-    genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
+    genv = iterate (fun ge -> Lazy.from_val Not_subterm::ge) n renv.genv }
 
 let push_fix_renv renv (_,v,_ as recdef) =
   let n = Array.length v in
   { env = push_rec_types recdef renv.env;
     rel_min = renv.rel_min+n;
-    genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
+    genv = iterate (fun ge -> Lazy.from_val Not_subterm::ge) n renv.genv }
 
 
 (* Definition and manipulation of the stack *)
@@ -628,14 +628,15 @@ let check_inductive_codomain env p =
 (* The following functions are almost duplicated from indtypes.ml, except
 that they carry here a poorer environment (containing less information). *)
 let ienv_push_var (env, lra) (x,a,ra) =
-(push_rel (x,None,a) env, (Norec,ra)::lra)
+(push_rel (LocalAssum (x,a)) env, (Norec,ra)::lra)
 
 let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
   let mib = Environ.lookup_mind mind env in
   let ntypes = mib.mind_ntypes in
   let push_ind specif env =
-     push_rel (Anonymous,None,
-		hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) env
+     let decl = LocalAssum (Anonymous,
+		            hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in
+     push_rel decl env
   in
   let env = Array.fold_right push_ind mib.mind_packets env in
   let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in
@@ -861,7 +862,7 @@ and stack_element_specif = function
   |SArg x -> x
 
 and extract_stack renv a = function
-  | [] -> Lazy.lazy_from_val Not_subterm , []
+  | [] -> Lazy.from_val Not_subterm , []
   | h::t -> stack_element_specif h, t
 
 
@@ -902,7 +903,7 @@ let filter_stack_domain env ci p stack =
     let t = whd_betadeltaiota env ar in
     match stack, t with
     | elt :: stack', Prod (n,a,c0) ->
-      let d = (n,None,a) in
+      let d = LocalAssum (n,a) in
       let ty, args = decompose_app (whd_betadeltaiota env a) in
       let elt = match ty with
       | Ind ind -> 
@@ -956,10 +957,10 @@ let check_one_fix renv recpos trees def =
               end
             else
               begin
-                match pi2 (lookup_rel p renv.env) with
-                | None ->
+                match lookup_rel p renv.env with
+                | LocalAssum _ ->
                     List.iter (check_rec_call renv []) l
-                | Some c ->
+                | LocalDef (_,c,_) ->
                     try List.iter (check_rec_call renv []) l
                     with FixGuardError _ ->
                       check_rec_call renv stack (applist(lift p c,l))
@@ -1078,7 +1079,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
       match (whd_betadeltaiota env def) with
         | Lambda (x,a,b) ->
 	    if noccur_with_meta n nbfix a then
-	      let env' = push_rel (x, None, a) env in
+	      let env' = push_rel (LocalAssum (x,a)) env in
               if n = k+1 then
                 (* get the inductive type of the fixpoint *)
                 let (mind, _) =
@@ -1127,7 +1128,7 @@ let rec codomain_is_coind env c =
   let b = whd_betadeltaiota env c in
   match b with
     | Prod (x,a,b) ->
-	codomain_is_coind (push_rel (x, None, a) env) b
+	codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
     | _ ->
 	(try find_coinductive env b
         with Not_found ->
@@ -1168,7 +1169,7 @@ let check_one_cofix env nbfix def deftype =
 	| Lambda (x,a,b) ->
 	     assert (args = []);
             if noccur_with_meta n nbfix a then
-              let env' = push_rel (x, None, a) env in
+              let env' = push_rel (LocalAssum (x,a)) env in
               check_rec_call env' alreadygrd (n+1) tree vlra b
             else
 	      raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
diff --git a/checker/inductive.mli b/checker/inductive.mli
index 78fb0bdd13..ed3a7b53ce 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 998e23c6e8..3ea5ed0d34 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -18,19 +18,27 @@ let refresh_arity ar =
   let ctxt, hd = decompose_prod_assum ar in
   match hd with
       Sort (Type u) when not (Univ.is_univ_variable u) ->
-        let u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in
-        mkArity (ctxt,Prop Null), 
-	  Univ.enforce_leq u u' Univ.empty_constraint
-    | _ -> ar, Univ.empty_constraint
+      let ul = Univ.Level.make empty_dirpath 1 in
+      let u' = Univ.Universe.make ul in
+      let cst = Univ.enforce_leq u u' Univ.empty_constraint in
+      let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in
+        mkArity (ctxt,Prop Null), ctx
+    | _ -> ar, Univ.ContextSet.empty
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn); pp_flush ();
-  let env' = add_constraints (Univ.UContext.constraints cb.const_universes) env in
+  let env' =
+    if cb.const_polymorphic then
+      let inst = Univ.make_abstract_instance cb.const_universes in
+      let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in
+        push_context ~strict:false ctx env
+    else push_context ~strict:true cb.const_universes env
+  in
   let envty, ty = 
     match cb.const_type with
       RegularArity ty ->
         let ty', cu = refresh_arity ty in
-        let envty = add_constraints cu env' in
+        let envty = push_context_set cu env' in
         let _ = infer_type envty ty' in envty, ty
     | TemplateArity(ctxt,par) ->
         let _ = check_ctxt env' ctxt in
@@ -69,7 +77,7 @@ let mk_mtb mp sign delta =
     mod_expr = Abstract;
     mod_type = sign;
     mod_type_alg = None;
-    mod_constraints = Univ.Constraint.empty;
+    mod_constraints = Univ.ContextSet.empty;
     mod_delta = delta;
     mod_retroknowledge = []; }
 
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index ae28caed09..5c7b392ffd 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/modops.ml b/checker/modops.ml
index 8ccf118d3b..9f43752620 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -83,12 +83,13 @@ let strengthen_const mp_from l cb resolver =
     | Def _ -> cb
     | _ ->
       let con = Constant.make2 mp_from l in
-      (* let con =  constant_of_delta resolver con in*)
       let u = 
-	if cb.const_polymorphic then Univ.UContext.instance cb.const_universes 
+	if cb.const_polymorphic then
+	  Univ.make_abstract_instance cb.const_universes
 	else Univ.Instance.empty
       in
-      { cb with const_body = Def (Declarations.from_val (Const (con,u))) }
+      { cb with
+	const_body = Def (Declarations.from_val (Const (con,u))) }
 
 let rec strengthen_mod mp_from mp_to mb =
   if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb
diff --git a/checker/modops.mli b/checker/modops.mli
index e22c2656c8..26a088f32b 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/print.ml b/checker/print.ml
index 7624fd3257..9cd8fda5dc 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 8ddeea2a20..f1aa5d9194 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -175,7 +175,7 @@ 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 "cort_cmp: %s\n%!" Pp.(string_of_ppcmds
+            Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds
               (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
                ++ Univ.pr_universes univ))
           end;
@@ -490,7 +490,7 @@ let dest_prod env =
     let t = whd_betadeltaiota env c in
     match t with
       | Prod (n,a,c0) ->
-          let d = (n,None,a) in
+          let d = LocalAssum (n,a) in
 	  decrec (push_rel d env) (d::m) c0
       | _ -> m,t
   in
@@ -502,10 +502,10 @@ let dest_prod_assum env =
     let rty = whd_betadeltaiota_nolet env ty in
     match rty with
     | Prod (x,t,c)  ->
-        let d = (x,None,t) in
+        let d = LocalAssum (x,t) in
 	prodec_rec (push_rel d env) (d::l) c
     | LetIn (x,b,t,c) ->
-        let d = (x,Some b,t) in
+        let d = LocalDef (x,b,t) in
 	prodec_rec (push_rel d env) (d::l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               ->
@@ -520,10 +520,10 @@ let dest_lam_assum env =
     let rty = whd_betadeltaiota_nolet env ty in
     match rty with
     | Lambda (x,t,c)  ->
-        let d = (x,None,t) in
+        let d = LocalAssum (x,t) in
 	lamec_rec (push_rel d env) (d::l) c
     | LetIn (x,b,t,c) ->
-        let d = (x,Some b,t) in
+        let d = LocalDef (x,b,t) in
 	lamec_rec (push_rel d env) (d::l) c
     | Cast (c,_,_)    -> lamec_rec env l c
     | _               -> l,rty
diff --git a/checker/reduction.mli b/checker/reduction.mli
index 2e87346980..2f551f4a6c 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index dd94823135..7f9ed92f95 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -13,6 +13,8 @@ open Cic
 open Names
 open Environ
 
+let pr_dirpath dp = str (DirPath.to_string dp)
+
 (************************************************************************)
 (*
  * Global environment
@@ -27,8 +29,8 @@ let set_engagement c =
 (* full_add_module adds module with universes and constraints *)
 let full_add_module dp mb univs digest =
   let env = !genv in
-  let env = add_constraints mb.mod_constraints env in
-  let env = add_constraints univs env in
+  let env = push_context_set ~strict:true mb.mod_constraints env in
+  let env = push_context_set ~strict:true univs env in
   let env = Modops.add_module mb env in
   genv := add_digest env dp digest
 
@@ -52,9 +54,9 @@ let check_engagement env (expected_impredicative_set,expected_type_in_type) =
 
 let report_clash f caller dir =
   let msg =
-    str "compiled library " ++ str(DirPath.to_string caller) ++
+    str "compiled library " ++ pr_dirpath caller ++
     spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++
-    str(DirPath.to_string dir) ++ fnl() in
+    pr_dirpath dir ++ fnl() in
   f msg
 
 
@@ -83,8 +85,8 @@ let import file clib univs digest =
   check_engagement env clib.comp_enga;
   let mb = clib.comp_mod in
   Mod_checking.check_module
-    (add_constraints univs
-      (add_constraints mb.mod_constraints env)) mb.mod_mp mb;
+    (push_context_set ~strict:true univs
+      (push_context_set ~strict:true mb.mod_constraints env)) mb.mod_mp mb;
   stamp_library file digest;
   full_add_module clib.comp_name mb univs digest
 
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index e16e64e6a2..8724f8e014 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -15,6 +15,6 @@ val get_env : unit -> env
 
 val set_engagement : engagement -> unit
 val import         :
-  CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit
+  CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit
 val unsafe_import  :
-  CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit
+  CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 372c314247..e41922573f 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/subtyping.mli b/checker/subtyping.mli
index 03242cbcfc..cc66fc5382 100644
--- a/checker/subtyping.mli
+++ b/checker/subtyping.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/term.ml b/checker/term.ml
index 430be49519..56cc9cdc22 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -222,24 +222,29 @@ let rel_context_length = List.length
 let rel_context_nhyps hyps =
   let rec nhyps acc = function
     | [] -> acc
-    | (_,None,_)::hyps -> nhyps (1+acc) hyps
-    | (_,Some _,_)::hyps -> nhyps acc hyps in
+    | LocalAssum _ :: hyps -> nhyps (1+acc) hyps
+    | LocalDef _ :: hyps -> nhyps acc hyps in
   nhyps 0 hyps
 let fold_rel_context f l ~init = List.fold_right f l init
 
-let map_rel_context f l =
-  let map_decl (n, body_o, typ as decl) =
-    let body_o' = Option.smartmap f body_o in
-    let typ' = f typ in
-      if body_o' == body_o && typ' == typ then decl else
-	(n, body_o', typ')
-  in
-    List.smartmap map_decl l
+let map_rel_decl f = function
+  | LocalAssum (n, typ) as decl ->
+     let typ' = f typ in
+     if typ' == typ then decl else
+       LocalAssum (n, typ')
+  | LocalDef (n, body, typ) as decl ->
+     let body' = f body in
+     let typ' = f typ in
+     if body' == body && typ' == typ then decl else
+       LocalDef (n, body', typ')
+
+let map_rel_context f =
+  List.smartmap (map_rel_decl f)
 
 let extended_rel_list n hyps =
   let rec reln l p = function
-    | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
-    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
+    | LocalDef _ :: hyps -> reln l (p+1) hyps
     | [] -> l
   in
   reln [] 1 hyps
@@ -272,8 +277,8 @@ let decompose_lam_n_assum n =
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else match c with
-    | Lambda (x,t,c)  -> lamdec_rec ((x,None,t) :: l) (n-1) c
-    | LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c
+    | Lambda (x,t,c)  -> lamdec_rec (LocalAssum (x,t) :: l) (n-1) c
+    | LetIn (x,b,t,c) -> lamdec_rec (LocalDef (x,b,t) :: l) n c
     | Cast (c,_,_)      -> lamdec_rec l n c
     | c -> error "decompose_lam_n_assum: not enough abstractions"
   in
@@ -282,18 +287,18 @@ let decompose_lam_n_assum n =
 (* Iterate products, with or without lets *)
 
 (* Constructs either [(x:t)c] or [[x=b:t]c] *)
-let mkProd_or_LetIn (na,body,t) c =
-  match body with
-    | None -> Prod (na, t, c)
-    | Some b -> LetIn (na, b, t, c)
+let mkProd_or_LetIn decl c =
+  match decl with
+    | LocalAssum (na,t) -> Prod (na, t, c)
+    | LocalDef (na,b,t) -> LetIn (na, b, t, c)
 
 let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
 
 let decompose_prod_assum =
   let rec prodec_rec l c =
     match c with
-    | Prod (x,t,c)    -> prodec_rec ((x,None,t) :: l) c
-    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) c
+    | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t) :: l) c
+    | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c
     | Cast (c,_,_)    -> prodec_rec l c
     | _               -> l,c
   in
@@ -305,8 +310,8 @@ let decompose_prod_n_assum n =
   let rec prodec_rec l n c =
     if Int.equal n 0 then l,c
     else match c with
-    | Prod (x,t,c)    -> prodec_rec ((x,None,t) :: l) (n-1) c
-    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c
+    | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t) :: l) (n-1) c
+    | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) (n-1) c
     | Cast (c,_,_)    -> prodec_rec l n c
     | c -> error "decompose_prod_n_assum: not enough assumptions"
   in
@@ -324,8 +329,8 @@ let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign
 let destArity =
   let rec prodec_rec l c =
     match c with
-    | Prod (x,t,c)    -> prodec_rec ((x,None,t)::l) c
-    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
+    | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t)::l) c
+    | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t)::l) c
     | Cast (c,_,_)    -> prodec_rec l c
     | Sort s          -> l,s
     | _               -> anomaly ~label:"destArity" (Pp.str "not an arity")
diff --git a/checker/term.mli b/checker/term.mli
index ab488b2b7c..0af83e05d7 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -35,12 +35,13 @@ val rel_context_length : rel_context -> int
 val rel_context_nhyps : rel_context -> int
 val fold_rel_context :
   (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration
 val map_rel_context : (constr -> constr) -> rel_context -> rel_context
 val extended_rel_list : int -> rel_context -> constr list
 val compose_lam : (name * constr) list -> constr -> constr
 val decompose_lam : constr -> (name * constr) list * constr
 val decompose_lam_n_assum : int -> constr -> rel_context * constr
-val mkProd_or_LetIn : name * constr option * constr -> constr -> constr
+val mkProd_or_LetIn : rel_declaration -> constr -> constr
 val it_mkProd_or_LetIn : constr -> rel_context -> constr
 val decompose_prod_assum : constr -> rel_context * constr
 val decompose_prod_n_assum : int -> constr -> rel_context * constr
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index c4c6528651..b7718e02da 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/type_errors.mli b/checker/type_errors.mli
index 036ff45462..d9d1479580 100644
--- a/checker/type_errors.mli
+++ b/checker/type_errors.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 21819992a9..64afd21b2a 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -62,7 +62,7 @@ let judge_of_type u = Sort (Type (Univ.super u))
 
 let judge_of_relative env n =
   try
-    let (_,_,typ) = lookup_rel n env in
+    let LocalAssum (_,typ) | LocalDef (_,_,typ) = lookup_rel n env in
     lift n typ
   with Not_found ->
     error_unbound_rel env n
@@ -296,13 +296,13 @@ let rec execute env cstr =
 
     | Lambda (name,c1,c2) ->
         let _ = execute_type env c1 in
-	let env1 = push_rel (name,None,c1) env in
+	let env1 = push_rel (LocalAssum (name,c1)) env in
         let j' = execute env1 c2 in
         Prod(name,c1,j')
 
     | Prod (name,c1,c2) ->
         let varj = execute_type env c1 in
-	let env1 = push_rel (name,None,c1) env in
+	let env1 = push_rel (LocalAssum (name,c1)) env in
         let varj' = execute_type env1 c2 in
 	Sort (sort_of_product env varj varj')
 
@@ -314,7 +314,7 @@ let rec execute env cstr =
           let env',c2' = (* refresh_arity env *) env, c2 in
           let _ = execute_type env' c2' in
           judge_of_cast env' (c1,j1) DEFAULTcast c2' in
-        let env1 = push_rel (name,Some c1,c2) env in
+        let env1 = push_rel (LocalDef (name,c1,c2)) env in
         let j' = execute env1 c3 in
         subst1 c1 j'
 
@@ -378,10 +378,10 @@ let infer_type env constr = execute_type env constr
 let check_ctxt env rels =
   fold_rel_context (fun d env ->
     match d with
-        (_,None,ty) ->
+      | LocalAssum (_,ty) ->
           let _ = infer_type env ty in
           push_rel d env
-      | (_,Some bd,ty) ->
+      | LocalDef (_,bd,ty) ->
           let j1 = infer env bd in
           let _ = infer env ty in
           conv_leq env j1 ty;
@@ -399,9 +399,9 @@ let check_polymorphic_arity env params par =
   let pl = par.template_param_levels in
   let rec check_p env pl params =
     match pl, params with
-        Some u::pl, (na,None,ty)::params ->
+        Some u::pl, LocalAssum (na,ty)::params ->
           check_kind env ty u;
-          check_p (push_rel (na,None,ty) env) pl params
+          check_p (push_rel (LocalAssum (na,ty)) env) pl params
       | None::pl,d::params -> check_p (push_rel d env) pl params
       | [], _ -> ()
       | _ -> failwith "check_poly: not the right number of params" in
diff --git a/checker/typeops.mli b/checker/typeops.mli
index 39d6604188..db8e467a33 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/univ.ml b/checker/univ.ml
index 3bcb3bc950..96d8270137 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -33,7 +33,7 @@ module type Hashconsed =
 sig
   type t
   val hash : t -> int
-  val equal : t -> t -> bool
+  val eq : t -> t -> bool
   val hcons : t -> t
 end
 
@@ -51,7 +51,7 @@ struct
     type t = _t
     type u = (M.t -> M.t)
     let hash = function Nil -> 0 | Cons (_, h, _) -> h
-    let equal l1 l2 = match l1, l2 with
+    let eq l1 l2 = match l1, l2 with
     | Nil, Nil -> true
     | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2
     | _ -> false
@@ -131,7 +131,7 @@ module HList = struct
   let rec remove x = function
   | Nil -> nil
   | Cons (y, _, l) ->
-    if H.equal x y then l
+    if H.eq x y then l
     else cons y (remove x l)
 
   end
@@ -229,7 +229,7 @@ module Level = struct
     type _t = t
     type t = _t
     type u = unit
-    let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data
+    let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data
     let hash x = x.hash
     let hashcons () x =
       let data' = RawLevel.hcons x.data in
@@ -244,7 +244,8 @@ module Level = struct
 
   let set = make Set
   let prop = make Prop
-
+  let var i = make (Var i)
+		  
   let is_small x = 
     match data x with
     | Level _ -> false
@@ -281,8 +282,8 @@ module Level = struct
 end
 
 (** Level sets and maps *)
-module LSet = Set.Make (Level)
-module LMap = Map.Make (Level)
+module LMap = HMap.Make (Level)
+module LSet = LMap.Set
 
 type 'a universe_map = 'a LMap.t
 
@@ -319,7 +320,7 @@ struct
       let hashcons hdir (b,n as x) = 
 	let b' = hdir b in 
 	  if b' == b then x else (b',n)
-      let equal l1 l2 =
+      let eq l1 l2 =
         l1 == l2 || 
         match l1,l2 with
 	| (b,n), (b',n') -> b == b' && n == n'
@@ -338,7 +339,7 @@ struct
       let hcons =
         Hashcons.simple_hcons H.generate H.hcons Level.hcons
       let hash = ExprHash.hash
-      let equal x y = x == y ||
+      let eq x y = x == y ||
         (let (u,n) = x and (v,n') = y in
            Int.equal n n' && Level.equal u v)
 
@@ -559,20 +560,26 @@ let repr g u =
   in
   repr_rec u
 
-(* [safe_repr] also search for the canonical representative, but
-   if the graph doesn't contain the searched universe, we add it. *)
-
-let safe_repr g u =
-  let rec safe_repr_rec u =
-    match UMap.find u g with
-      | Equiv v -> safe_repr_rec v
-      | Canonical arc -> arc
-  in
-  try g, safe_repr_rec u
-  with Not_found ->
-    let can = terminal u in
-    enter_arc can g, can
+let get_set_arc g = repr g Level.set
 
+exception AlreadyDeclared
+	    
+let add_universe vlev strict g =
+  try
+    let _arcv = UMap.find vlev g in
+      raise AlreadyDeclared
+  with Not_found -> 
+    let v = terminal vlev in
+    let arc =
+      let arc = get_set_arc g in
+	if strict then
+	  { arc with lt=vlev::arc.lt}
+	else 
+	  { arc with le=vlev::arc.le}
+    in
+    let g = enter_arc arc g in
+      enter_arc v g
+		       
 (* reprleq : canonical_arc -> canonical_arc list *)
 (* All canonical arcv such that arcu<=arcv with arcv#arcu *)
 let reprleq g arcu =
@@ -739,8 +746,8 @@ let is_lt g arcu arcv =
 (** First, checks on universe levels *)
 
 let check_equal g u v =
-  let g, arcu = safe_repr g u in
-  let _, arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
   arcu == arcv
 
 let check_eq_level g u v = u == v || check_equal g u v
@@ -749,8 +756,8 @@ let is_set_arc u = Level.is_set u.univ
 let is_prop_arc u = Level.is_prop u.univ
 
 let check_smaller g strict u v =
-  let g, arcu = safe_repr g u in
-  let g, arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
   if strict then
     is_lt g arcu arcv
   else
@@ -900,8 +907,8 @@ let error_inconsistency o u v =
 (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
 
 let enforce_univ_eq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastEQ -> g
     | FastLT -> error_inconsistency Eq v u
@@ -916,8 +923,8 @@ let enforce_univ_eq u v g =
 (* enforce_univ_leq : Level.t -> Level.t -> unit *)
 (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
 let enforce_univ_leq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
   if is_leq g arcu arcv then g
   else
     match fast_compare g arcv arcu with
@@ -928,8 +935,8 @@ let enforce_univ_leq u v g =
 
 (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
 let enforce_univ_lt u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastLT -> g
     | FastLE -> fst (setlt g arcu arcv)
@@ -941,7 +948,10 @@ let enforce_univ_lt u v g =
       | FastLE | FastLT -> error_inconsistency Lt u v
 
 (* Prop = Set is forbidden here. *)
-let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty
+let initial_universes =
+  let g = enter_arc (terminal Level.set) UMap.empty in
+  let g = enter_arc (terminal Level.prop) g in
+    enforce_univ_lt Level.prop Level.set g
 
 (* Constraints and sets of constraints. *)    
 
@@ -970,7 +980,7 @@ module Constraint = Set.Make(UConstraintOrd)
 let empty_constraint = Constraint.empty
 let merge_constraints c g =
   Constraint.fold enforce_constraint c g
-
+		  
 type constraints = Constraint.t
 
 (** A value with universe constraints. *)
@@ -1079,7 +1089,7 @@ struct
 	  a
 	end
 
-    let equal t1 t2 =
+    let eq t1 t2 =
       t1 == t2 ||
 	(Int.equal (Array.length t1) (Array.length t2) &&
 	   let rec aux i =
@@ -1146,7 +1156,7 @@ struct
 
   (** Universe contexts (variables as a list) *)
   let empty = (Instance.empty, Constraint.empty)
-
+  let make x = x
   let instance (univs, cst) = univs
   let constraints (univs, cst) = cst
 end
@@ -1158,6 +1168,8 @@ struct
   type t = LSet.t constrained
   let empty = LSet.empty, Constraint.empty
   let constraints (_, cst) = cst
+  let levels (ctx, _) = ctx
+  let make ctx cst = (ctx, cst)
 end
 type universe_context_set = ContextSet.t
 
@@ -1207,6 +1219,9 @@ let subst_instance_constraints s csts =
     (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
     csts Constraint.empty 
 
+let make_abstract_instance (ctx, _) = 
+  Array.mapi (fun i l -> Level.var i) ctx
+
 (** Substitute instance inst for ctx in csts *)
 let instantiate_univ_context (ctx, csts) = 
   (ctx, subst_instance_constraints ctx csts)
@@ -1238,6 +1253,20 @@ let subst_univs_universe fn ul =
 	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u))
 	  substs nosubst
 
+let merge_context strict ctx g =
+  let g = Array.fold_left
+   (* Be lenient, module typing reintroduces universes and 
+      constraints due to includes *)
+	    (fun g v -> try add_universe v strict g with AlreadyDeclared -> g)
+	    g (UContext.instance ctx)
+  in merge_constraints (UContext.constraints ctx) g
+
+let merge_context_set strict ctx g =
+  let g = LSet.fold
+	    (fun v g -> try add_universe v strict g with AlreadyDeclared -> g)
+	    (ContextSet.levels ctx) g
+  in merge_constraints (ContextSet.constraints ctx) g
+
 (** Pretty-printing *)
 
 let pr_arc = function
diff --git a/checker/univ.mli b/checker/univ.mli
index 742ef91aed..7d4c629ab9 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -74,6 +74,13 @@ val check_eq : universe check_function
 (** The initial graph of universes: Prop < Set *)
 val initial_universes : universes
 
+(** Adds a universe to the graph, ensuring it is >= or > Set.
+   @raises AlreadyDeclared if the level is already declared in the graph. *)
+
+exception AlreadyDeclared
+
+val add_universe : universe_level -> bool -> universes -> universes
+
 (** {6 Constraints. } *)
 
 type constraint_type = Lt | Le | Eq
@@ -117,14 +124,14 @@ type univ_inconsistency = constraint_type * universe * universe
 exception UniverseInconsistency of univ_inconsistency
 
 val merge_constraints : constraints -> universes -> universes
-
+						    
 val check_constraints : constraints -> universes -> bool
 
 (** {6 Support for universe polymorphism } *)
 
 (** Polymorphic maps from universe levels to 'a *)
-module LMap : Map.S with type key = universe_level
-
+module LMap : CSig.MapS with type key = universe_level
+module LSet : CSig.SetS with type elt = universe_level
 type 'a universe_map = 'a LMap.t
 
 (** {6 Substitution} *)
@@ -177,7 +184,7 @@ sig
   type t
 
   val empty : t
-
+  val make : universe_instance constrained -> t
   val instance : t -> Instance.t
   val constraints : t -> constraints
 
@@ -186,6 +193,7 @@ end
 module ContextSet :
   sig 
     type t
+    val make : LSet.t -> constraints -> t
     val empty : t
     val constraints : t -> constraints
   end
@@ -193,6 +201,9 @@ module ContextSet :
 type universe_context = UContext.t
 type universe_context_set = ContextSet.t
 
+val merge_context : bool -> universe_context -> universes -> universes
+val merge_context_set : bool -> universe_context_set -> universes -> universes
+
 val empty_level_subst : universe_level_subst
 val is_empty_level_subst : universe_level_subst -> bool
 
@@ -219,6 +230,9 @@ val subst_instance_constraints : universe_instance -> constraints -> constraints
 val instantiate_univ_context : universe_context -> universe_context
 val instantiate_univ_constraints : universe_instance -> universe_context -> constraints
 
+(** Build the relative instance corresponding to the context *)
+val make_abstract_instance : universe_context -> universe_instance
+									    
 (** {6 Pretty-printing of universes. } *)
 
 val pr_universes : universes -> Pp.std_ppcmds
diff --git a/checker/validate.ml b/checker/validate.ml
index 63180f055e..c434ef09d3 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/values.ml b/checker/values.ml
index 45220bd051..19cbb50606 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 8b7e75b4b94a2d8506a62508e0374c0a checker/cic.mli
+MD5 9f7fd499f812b6548a55f7067e6a9d06 checker/cic.mli
 
 *)
 
@@ -154,8 +154,8 @@ and v_prec = Tuple ("prec_declaration",
 and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|])
 and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|])
 
-
-let v_rdecl = v_tuple "rel_declaration" [|v_name;Opt v_constr;v_constr|]
+let v_rdecl = v_sum "rel_declaration" 0 [| [|v_name; v_constr|];               (* LocalAssum *)
+                                           [|v_name; v_constr; v_constr|] |]   (* LocalDef *)
 let v_rctxt = List v_rdecl
 
 let v_section_ctxt = v_enum "emptylist" 1
@@ -307,10 +307,10 @@ and v_impl =
 and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *)
 and v_module =
   Tuple ("module_body",
-         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|])
+         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
 and v_modtype =
   Tuple ("module_type_body",
-         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|])
+         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
 
 (** kernel/safe_typing *)
 
diff --git a/checker/votour.ml b/checker/votour.ml
index 4aecb28f20..79755da4ad 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -22,6 +22,7 @@ sig
   val input : in_channel -> obj
   val repr : obj -> obj repr
   val size : obj -> int
+  val oid : obj -> int option
 end
 
 module ReprObj : S =
@@ -45,6 +46,7 @@ struct
     else INT (Obj.magic obj)
 
   let size (_, p) = CObj.shared_size_of_pos p
+  let oid _ = None
 end
 
 module ReprMem : S =
@@ -97,6 +99,9 @@ struct
     let _ = init_size seen obj in
     obj
 
+  let oid = function
+  | Int _ | Atm _ | Fun _ -> None
+  | Ptr p -> Some p
 end
 
 module Visit (Repr : S) :
@@ -149,9 +154,13 @@ let rec get_details v o = match v, Repr.repr o with
   |Annot (s,v), _ -> get_details v o
   |_ -> ""
 
+let get_oid obj = match Repr.oid obj with
+| None -> ""
+| Some id -> Printf.sprintf " [0x%08x]" id
+
 let node_info (v,o,p) =
   get_name ~extra:true v ^ get_details v o ^
-    " (size "^ string_of_int (Repr.size o)^"w)"
+    " (size "^ string_of_int (Repr.size o)^"w)" ^ get_oid o
 
 (** Children of a block : type, object, position.
     For lists, we collect all elements of the list at once *)