Merge branch 'v8.5'

78 files changed, 581 insertions, 416 deletions

diff --git a/CHANGES b/CHANGES
index 050d3e999..733bcc7cf 100644
--- a/CHANGES
+++ b/CHANGES
@@ -161,7 +161,7 @@ Specification Language
   break user notations using "$(", fixable by inserting a space or
   rewriting the notation).
 - Constructors in pattern-matching patterns now respect the same rules
-  regarding implicit arguments than in applicative position. The old
+  regarding implicit arguments as in applicative position. The old
   behavior can be recovered by the command "Set Asymmetric
   Patterns". As a side effect, notations for constructors explicitly
   mentioning non-implicit parameters can now be used in patterns.
@@ -188,10 +188,12 @@ Tactics
     during the execution of c, it can backtrack and try b instead of a.
   * New tactical (once a) removes all the backtracking points from a
     (i.e. it selects the first success of a).
-  * Tactic "constructor" is now fully backtracking, thus deprecating
-    the need of the undocumented "constructor <tac>" syntax which is
-    now equivalent to "[> once (constructor; tac) ..]". (potential
-    source of rare incompatibilities).
+  * Tactic "constructor" is now fully backtracking. In case of
+    incompatibilities (e.g. combinatoric explosion), the former
+    behavior of "constructor" can be retrieved by using instead
+    "[> once constructor ..]". Thanks to backtracking, undocumented
+    "constructor <tac>" syntax is now equivalent to
+    "[> once (constructor; tac) ..]".
   * New "multimatch" variant of "match" tactic which backtracks to
     new branches in case of a later failure. The "match" tactic is
     equivalent to "once multimatch".
diff --git a/Makefile.build b/Makefile.build
index 623428328..6650427e6 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -282,11 +282,11 @@ $(COQC):  $(patsubst %.cma,%$(BESTLIB),$(COQCCMO:.cmo=$(BESTOBJ)))
 
 # For the checker, different flags may be used
 
-checker/check.cma: | checker/check.mllib.d
+checker/check.cma: | md5chk checker/check.mllib.d
 	$(SHOW)'OCAMLC -a -o $@'
 	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $^
 
-checker/check.cmxa: | checker/check.mllib.d
+checker/check.cmxa: | md5chk checker/check.mllib.d
 	$(SHOW)'OCAMLOPT -a -o $@'
 	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $^
 
@@ -479,7 +479,7 @@ md5chk:
 
 VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m
 
-validate: $(CHICKEN) md5chk | $(ALLVO)
+validate: $(CHICKEN) | $(ALLVO)
 	$(SHOW)'COQCHK <theories & plugins>'
 	$(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
 
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 05a2a1b99..d041f1b7e 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -23,11 +23,17 @@ let print_memory_stat () =
 
 let output_context = ref false
 
-let pr_engt = function
-    Some ImpredicativeSet ->
-      str "Theory: Set is impredicative"
-  | None ->
-      str "Theory: Set is predicative"
+let pr_engagement (impr_set,type_in_type) =
+  begin
+    match impr_set with
+    | ImpredicativeSet -> str "Theory: Set is impredicative"
+    | PredicativeSet -> str "Theory: Set is predicative"
+  end ++
+  begin
+    match type_in_type with
+    | StratifiedType -> str "Theory: Stratified type hierarchy"
+    | TypeInType -> str "Theory: Type is of type Type"
+  end
 
 let cst_filter f csts =
   Cmap_env.fold
@@ -54,7 +60,7 @@ let print_context env =
     ppnl(hov 0
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
-      str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_ax csts) ++
       fnl())); pp_flush()
   end
diff --git a/checker/checker.ml b/checker/checker.ml
index 0f7ed8df5..d5d9b9e3b 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -138,10 +138,11 @@ let init_load_path () =
 
 let set_debug () = Flags.debug := true
 
-let engagement = ref None
-let set_engagement c = engagement := Some c
-let engage () =
-  match !engagement with Some c -> Safe_typing.set_engagement c | None -> ()
+let impredicative_set = ref Cic.PredicativeSet
+let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet
+let type_in_type = ref Cic.StratifiedType
+let set_type_in_type () = type_in_type := Cic.TypeInType
+let engage () = Safe_typing.set_engagement (!impredicative_set,!type_in_type)
 
 
 let admit_list = ref ([] : section_path list)
@@ -194,6 +195,7 @@ let print_usage_channel co command =
 \n  -silent                disable trace of constants being checked\
 \n\
 \n  -impredicative-set     set sort Set impredicative\
+\n  -type-in-type          collapse type hierarchy\
 \n\
 \n  -h, --help             print this list of options\
 \n"
@@ -319,7 +321,9 @@ let parse_args argv =
   let rec parse = function
     | [] -> ()
     | "-impredicative-set" :: rem ->
-      set_engagement Cic.ImpredicativeSet; parse rem
+      set_impredicative_set (); parse rem
+    | "-type-in-type" :: rem ->
+      set_type_in_type (); parse rem
 
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then 
diff --git a/checker/cic.mli b/checker/cic.mli
index e875e40f0..881d3ca79 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -102,7 +102,7 @@ type constr =
   | Case      of case_info * constr * constr * constr array
   | Fix       of constr pfixpoint
   | CoFix     of constr pcofixpoint
-  | Proj      of constant * constr
+  | Proj      of projection * constr
 
 type existential = constr pexistential
 type rec_declaration = constr prec_declaration
@@ -165,7 +165,10 @@ type action
 
 (** Engagements *)
 
-type engagement = ImpredicativeSet
+type set_predicativity = ImpredicativeSet | PredicativeSet
+type type_hierarchy = TypeInType | StratifiedType
+
+type engagement = set_predicativity * type_hierarchy
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
@@ -407,7 +410,7 @@ type compiled_library = {
   comp_name : compilation_unit_name;
   comp_mod : module_body;
   comp_deps : library_deps;
-  comp_enga : engagement option;
+  comp_enga : engagement;
   comp_natsymbs : nativecode_symb_array
 }
 
diff --git a/checker/closure.ml b/checker/closure.ml
index 356b683fa..c6cc2185d 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -276,7 +276,7 @@ and fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of constant * fconstr
+  | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCase of case_info * fconstr * fconstr * fconstr array
@@ -308,7 +308,7 @@ type stack_member =
   | Zapp of fconstr array
   | Zcase of case_info * fconstr * fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * constant
+  | Zproj of int * int * projection
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -678,8 +678,9 @@ let eta_expand_ind_stack env ind m s (f, s') =
       let (depth, args, s) = strip_update_shift_app m s in
       (** Try to drop the params, might fail on partially applied constructors. *)
       let argss = try_drop_parameters depth pars args in
-      let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
-					 term = FProj (p, right) }) projs in
+	let hstack =
+	  Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
+			     term = FProj (Projection.make p false, right) }) projs in
 	argss, [Zapp hstack]	
     | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
@@ -738,7 +739,7 @@ let rec knh info m stk =
     | FCast(t,_,_) -> knh info t stk
 
     | FProj (p,c) ->
-      if red_set info.i_flags (fCONST p) then
+      if red_set info.i_flags (fCONST (Projection.constant p)) then
         (let pb = lookup_projection p (info.i_env) in
 	   knh info c (Zproj (pb.proj_npars, pb.proj_arg, p)
 		       :: zupdate m stk))
diff --git a/checker/closure.mli b/checker/closure.mli
index e6b39250d..376e9fef7 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -95,7 +95,7 @@ type fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of constant * fconstr
+  | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCase of case_info * fconstr * fconstr * fconstr array
@@ -117,7 +117,7 @@ type stack_member =
   | Zapp of fconstr array
   | Zcase of case_info * fconstr * fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * constant
+  | Zproj of int * int * projection
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 8d913475f..36e6a7cab 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -206,14 +206,15 @@ let rec map_kn f f' c =
   let func = map_kn f f' in
     match c with
       | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c)
-      | Proj (kn,t) -> 
-          let kn' = 
-	    try fst (f' kn Univ.Instance.empty)
-	    with No_subst -> kn 
+      | Proj (p,t) -> 
+          let p' = 
+	    Projection.map (fun kn ->
+			    try fst (f' kn Univ.Instance.empty)
+			    with No_subst -> kn) p
 	  in
 	  let t' = func t in
-	    if kn' == kn && t' == t then c
-	    else Proj (kn', t')
+	    if p' == p && t' == t then c
+	    else Proj (p', t')
       | Ind ((kn,i),u) ->
 	  let kn' = f kn in
 	  if kn'==kn then c else Ind ((kn',i),u)
diff --git a/checker/environ.ml b/checker/environ.ml
index 710ebc712..6dbc44d6b 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -14,7 +14,7 @@ type globals = {
 
 type stratification = {
   env_universes : Univ.universes;
-  env_engagement : engagement option
+  env_engagement : engagement
 }
 
 type env = {
@@ -33,19 +33,28 @@ let empty_env = {
   env_rel_context = [];
   env_stratification =
   { env_universes = Univ.initial_universes;
-    env_engagement = None};
+    env_engagement = (PredicativeSet,StratifiedType)};
   env_imports = MPmap.empty }
 
 let engagement env = env.env_stratification.env_engagement
 let universes env = env.env_stratification.env_universes
 let rel_context env = env.env_rel_context
 
-let set_engagement c env =
-  match env.env_stratification.env_engagement with
-    | Some c' -> if c=c' then env else error "Incompatible engagement"
-    | None ->
-        { env with env_stratification =
-          { env.env_stratification with env_engagement = Some c } }
+let set_engagement (impr_set,type_in_type as c) env =
+  let expected_impr_set,expected_type_in_type =
+    env.env_stratification.env_engagement in
+  begin
+    match impr_set,expected_impr_set with
+    | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement"
+    | _ -> ()
+  end;
+  begin
+    match type_in_type,expected_type_in_type with
+    | StratifiedType, TypeInType -> error "Incompatible engagement"
+    | _ -> ()
+  end;
+  { env with env_stratification =
+      { env.env_stratification with env_engagement = c } }
 
 (* Digests *)
 
@@ -147,8 +156,8 @@ let evaluable_constant cst env =
 let is_projection cst env = 
   not (Option.is_empty (lookup_constant cst env).const_proj)
 
-let lookup_projection cst env =
-  match (lookup_constant cst env).const_proj with 
+let lookup_projection p env =
+  match (lookup_constant (Projection.constant p) env).const_proj with 
   | Some pb -> pb
   | None -> anomaly ("lookup_projection: constant is not a projection")
 
diff --git a/checker/environ.mli b/checker/environ.mli
index d3448b127..f3b2dd839 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -11,7 +11,7 @@ type globals = {
   env_modtypes : module_type_body MPmap.t}
 type stratification = {
   env_universes : Univ.universes;
-  env_engagement : engagement option;
+  env_engagement : engagement;
 }
 type env = {
   env_globals : globals;
@@ -22,7 +22,7 @@ type env = {
 val empty_env : env
 
 (* Engagement *)
-val engagement : env -> Cic.engagement option
+val engagement : env -> Cic.engagement
 val set_engagement : Cic.engagement -> env -> env
 
 (* Digests *)
@@ -51,7 +51,7 @@ val constant_value : env -> constant puniverses -> constr
 val evaluable_constant : constant -> env -> bool
 
 val is_projection : constant -> env -> bool
-val lookup_projection : constant -> env -> projection_body
+val lookup_projection : projection -> env -> projection_body
 
 (* Inductives *)
 val mind_equiv : env -> inductive -> inductive -> bool
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 050c33e60..e1a6bc7c1 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -176,7 +176,7 @@ let typecheck_arity env params inds =
 (* Allowed eliminations *)
 
 let check_predicativity env s small level =
-  match s, engagement env with
+  match s, fst (engagement env) with
       Type u, _ ->
         (* let u' = fresh_local_univ () in *)
         (* let cst = *)
@@ -184,7 +184,7 @@ let check_predicativity env s small level =
         (*     (universes env) in *)
         if not (Univ.check_leq (universes env) level u) then
           failwith "impredicative Type inductive type"
-    | Prop Pos, Some ImpredicativeSet -> ()
+    | Prop Pos, ImpredicativeSet -> ()
     | Prop Pos, _ ->
         if not small then failwith "impredicative Set inductive type"
     | Prop Null,_ -> ()
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 59d1a645a..21b80f323 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -103,13 +103,12 @@ let instantiate_params full t u args sign =
 
 let full_inductive_instantiate mib u params sign =
   let dummy = Prop Null in
-  let t = mkArity (sign,dummy) in
+  let t = mkArity (subst_instance_context u sign,dummy) in
     fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
 
-let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
-  let inst_ind = constructor_instantiate mind u mib in
-  (fun t ->
-    instantiate_params true (inst_ind t) u params mib.mind_params_ctxt)
+let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
+  let inst_ind = constructor_instantiate mind u mib t in
+    instantiate_params true inst_ind u params mib.mind_params_ctxt
 
 (************************************************************************)
 (************************************************************************)
@@ -142,53 +141,60 @@ let sort_as_univ = function
 | Prop Null -> Univ.type0m_univ
 | Prop Pos -> Univ.type0_univ
 
+(* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
+(* in the domain or add [u |-> sup x su] if [u] is already mapped *)
+(* to [x]. *)
 let cons_subst u su subst =
-  Univ.LMap.add u su subst
-
-let actualize_decl_level env lev t =
-  let sign,s = dest_arity env t in
-  mkArity (sign,lev)
-
-let polymorphism_on_non_applied_parameters = false
+  try
+    Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+  with Not_found -> Univ.LMap.add u su subst
+
+(* remember_subst updates the mapping [u |-> x] by [u |-> sup x u] *)
+(* if it is presents and returns the substitution unchanged if not.*)
+let remember_subst u subst =
+  try
+    let su = Universe.make u in
+    Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+  with Not_found -> subst
 
 (* Bind expected levels of parameters to actual levels *)
 (* Propagate the new levels in the signature *)
-let rec make_subst env = function
-  | (_,Some _,_ as t)::sign, exp, args ->
-      let ctx,subst = make_subst env (sign, exp, args) in
-      t::ctx, subst
-  | d::sign, None::exp, args ->
-      let args = match args with _::args -> args | [] -> [] in
-      let ctx,subst = make_subst env (sign, exp, args) in
-      d::ctx, subst
-  | d::sign, Some u::exp, a::args ->
-      (* We recover the level of the argument, but we don't change the *)
-      (* level in the corresponding type in the arity; this level in the *)
-      (* arity is a global level which, at typing time, will be enforce *)
-      (* to be greater than the level of the argument; this is probably *)
-      (* a useless extra constraint *)
-      let s = sort_as_univ (snd (dest_arity env a)) in
-      let ctx,subst = make_subst env (sign, exp, args) in
-      d::ctx, cons_subst u s subst
-  | (na,None,t as d)::sign, Some u::exp, [] ->
-      (* No more argument here: we instantiate the type with a fresh level *)
-      (* which is first propagated to the corresponding premise in the arity *)
-      (* (actualize_decl_level), then to the conclusion of the arity (via *)
-      (* the substitution) *)
-      let ctx,subst = make_subst env (sign, exp, []) in
-	d::ctx, subst
-  | sign, [], _ ->
-      (* Uniform parameters are exhausted *)
-      sign,Univ.LMap.empty
-  | [], _, _ ->
-      assert false
-
+let rec make_subst env =
+  let rec make subst = function
+    | (_,Some _,_)::sign, exp, args ->
+        make subst (sign, exp, args)
+    | d::sign, None::exp, args ->
+        let args = match args with _::args -> args | [] -> [] in
+        make subst (sign, exp, args)
+    | d::sign, Some u::exp, a::args ->
+        (* We recover the level of the argument, but we don't change the *)
+        (* level in the corresponding type in the arity; this level in the *)
+        (* arity is a global level which, at typing time, will be enforce *)
+        (* to be greater than the level of the argument; this is probably *)
+        (* a useless extra constraint *)
+        let s = sort_as_univ (snd (dest_arity env a)) in
+        make (cons_subst u s subst) (sign, exp, args)
+    | (na,None,t)::sign, Some u::exp, [] ->
+        (* No more argument here: we add the remaining universes to the *)
+        (* substitution (when [u] is distinct from all other universes in the *)
+        (* template, it is identity substitution  otherwise (ie. when u is *)
+        (* already in the domain of the substitution) [remember_subst] will *)
+        (* update its image [x] by [sup x u] in order not to forget the *)
+        (* dependency in [u] that remains to be fullfilled. *)
+        make (remember_subst u subst) (sign, exp, [])
+    | sign, [], _ ->
+        (* Uniform parameters are exhausted *)
+        subst
+    | [], _, _ ->
+        assert false
+  in
+  make Univ.LMap.empty
 
 exception SingletonInductiveBecomesProp of Id.t
 
 let instantiate_universes env ctx ar argsorts =
   let args = Array.to_list argsorts in
-  let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
+  let subst = make_subst env (ctx,ar.template_param_levels,args) in
   let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
diff --git a/checker/print.ml b/checker/print.ml
index 1cc48ff77..7624fd325 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -100,7 +100,7 @@ let print_pure_constr csr =
         done
       in print_string"{"; print_fix (); print_string"}"
   | Proj (p, c) ->
-    print_string "Proj("; sp_con_display p; print_string ","; 
+    print_string "Proj("; sp_con_display (Projection.constant p); print_string ","; 
     box_display c; print_string ")"
 
   and box_display c = open_hovbox 1; term_display c; close_box()
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 28fdb130e..8ddeea2a2 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -52,7 +52,7 @@ let compare_stack_shape stk1 stk2 =
 
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
-  | Zlproj of Names.constant * lift
+  | Zlproj of Names.projection * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
   | Zlcase of case_info * lift * fconstr * fconstr array
 and lft_constr_stack = lft_constr_stack_elt list
@@ -137,7 +137,9 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
                 f fx1 fx2; cmp_rec a1 a2
 	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
-	      if not (Names.eq_con_chk c1 c2) then 
+	       if not (Names.eq_con_chk
+		       (Names.Projection.constant c1)
+		       (Names.Projection.constant c2)) then 
 		raise NotConvertible
             | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
                 if not (fmind ci1.ci_ind ci2.ci_ind) then
@@ -156,7 +158,7 @@ type conv_pb =
   | CONV
   | CUMUL
 
-let sort_cmp univ pb s0 s1 =
+let sort_cmp env univ pb s0 s1 =
   match (s0,s1) with
     | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible
     | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
@@ -165,7 +167,8 @@ let sort_cmp univ pb s0 s1 =
             CUMUL -> ()
           | _ -> raise NotConvertible)
     | (Type u1, Type u2) ->
-        if not
+        if snd (engagement env) == StratifiedType
+          && not
 	  (match pb with
             | CONV -> Univ.check_eq univ u1 u2
 	    | CUMUL -> Univ.check_leq univ u1 u2)
@@ -259,7 +262,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
 	(match a1, a2 with
 	   | (Sort s1, Sort s2) ->
 	       assert (is_empty_stack v1 && is_empty_stack v2);
-	       sort_cmp univ cv_pb s1 s2
+	       sort_cmp (infos_env infos) univ cv_pb s1 s2
 	   | (Meta n, Meta m) ->
                if n=m
 	       then convert_stacks univ infos lft1 lft2 v1 v2
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 810d6e0b6..dd9482313 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -32,13 +32,21 @@ let full_add_module dp mb univs digest =
   let env = Modops.add_module mb env in
   genv := add_digest env dp digest
 
-(* Check that the engagement expected by a library matches the initial one *)
-let check_engagement env c =
-  match engagement env, c with
-    | Some ImpredicativeSet, Some ImpredicativeSet -> ()
-    | _, None -> ()
-    | _, Some ImpredicativeSet ->
-        error "Needs option -impredicative-set"
+(* Check that the engagement expected by a library extends the initial one *)
+let check_engagement env (expected_impredicative_set,expected_type_in_type) =
+  let impredicative_set,type_in_type = Environ.engagement env in
+  begin
+    match impredicative_set, expected_impredicative_set with
+    | PredicativeSet, ImpredicativeSet ->
+        Errors.error "Needs option -impredicative-set."
+    | _ -> ()
+  end;
+  begin
+    match type_in_type, expected_type_in_type with
+    | StratifiedType, TypeInType ->
+        Errors.error "Needs option -type-in-type."
+    | _ -> ()
+  end
 
 (* Libraries = Compiled modules *)
 
diff --git a/checker/term.ml b/checker/term.ml
index 93540276b..430be4951 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -392,7 +392,7 @@ let compare_constr f t1 t2 =
       Array.equal f tl1 tl2 && Array.equal f bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
       Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
-  | Proj (p1,c1), Proj(p2,c2) -> eq_con_chk p1 p2 && f c1 c2
+  | Proj (p1,c1), Proj(p2,c2) -> Projection.equal p1 p2 && f c1 c2
   | _ -> false
 
 let rec eq_constr m n =
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 9bc4b269b..21819992a 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -128,7 +128,7 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        if engagement env = Some ImpredicativeSet then
+        if fst (engagement env) = ImpredicativeSet then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
         else
diff --git a/checker/values.ml b/checker/values.ml
index b2d74821d..45220bd05 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 f5fd749af797e08efee22122742bc740 checker/cic.mli
+MD5 8b7e75b4b94a2d8506a62508e0374c0a checker/cic.mli
 
 *)
 
@@ -126,6 +126,7 @@ let v_caseinfo =
   v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
 
 let v_cast = v_enum "cast_kind" 4
+let v_proj = v_tuple "projection" [|v_cst; v_bool|]
 
 let rec v_constr =
   Sum ("constr",0,[|
@@ -145,7 +146,7 @@ let rec v_constr =
     [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
     [|v_fix|]; (* Fix *)
     [|v_cofix|]; (* CoFix *)
-    [|v_cst;v_constr|] (* Proj *)
+    [|v_proj;v_constr|] (* Proj *)
   |])
 
 and v_prec = Tuple ("prec_declaration",
@@ -192,7 +193,9 @@ let v_lazy_constr =
 
 (** kernel/declarations *)
 
-let v_engagement = v_enum "eng" 1
+let v_impredicative_set = v_enum "impr-set" 2
+let v_type_in_type = v_enum "type-in-type" 2
+let v_engagement = v_tuple "eng" [|v_impredicative_set; v_type_in_type|]
 
 let v_pol_arity =
   v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
@@ -205,8 +208,10 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
 
 let v_projbody =
-  v_tuple "projection_body" [|v_cst;Int;Int;v_constr;v_tuple "proj_eta" [|v_constr;v_constr|];
-			      v_constr|]
+  v_tuple "projection_body"
+	  [|v_cst;Int;Int;v_constr;
+	    v_tuple "proj_eta" [|v_constr;v_constr|];
+	    v_constr|]
 
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
@@ -312,7 +317,7 @@ and v_modtype =
 let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
 let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
 let v_compiled_lib =
-  v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|]
+  v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|]
 
 (** Library objects *)
 
diff --git a/configure.ml b/configure.ml
index a1c172cf4..83468f8f3 100644
--- a/configure.ml
+++ b/configure.ml
@@ -372,7 +372,7 @@ let coq_annotate_flag =
   then if program_in_path "ocamlmerlin" then "-bin-annot" else "-dtypes"
   else ""
 
-let cflags = "-Wall -Wno-unused -g " ^ (if !Prefs.debug then "-O1" else "-O2")
+let cflags = "-Wall -Wno-unused -g -O2"
 
 (** * Architecture *)
 
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
index b1c278ced..a3372c296 100644
--- a/doc/refman/CanonicalStructures.tex
+++ b/doc/refman/CanonicalStructures.tex
@@ -41,25 +41,25 @@ End EQ.
 We use Coq modules as name spaces.  This allows us to follow the same pattern
 and naming convention for the rest of the chapter.  The base name space
 contains the definitions of the algebraic structure.  To keep the example
-small, the algebraic structure $EQ.type$ we are defining is very simplistic,
+small, the algebraic structure \texttt{EQ.type} we are defining is very simplistic,
 and characterizes terms on which a binary relation is defined, without
 requiring such relation to validate any property.
-The inner $theory$ module contains the overloaded notation $==$ and
+The inner \texttt{theory} module contains the overloaded notation \texttt{==} and
 will eventually contain lemmas holding on all the instances of the
 algebraic structure (in this case there are no lemmas).
 
-Note that in practice the user may want to declare $EQ.obj$ as a coercion,
+Note that in practice the user may want to declare \texttt{EQ.obj} as a coercion,
 but we will not do that here.
 
-The following line tests that, when we assume a type $e$ that is in the
-$EQ$ class, then we can relates two of its objects with $==$.
+The following line tests that, when we assume a type \texttt{e} that is in the
+\texttt{EQ} class, then we can relates two of its objects with \texttt{==}.
 
 \begin{coq_example}
 Import EQ.theory.
 Check forall (e : EQ.type) (a b : EQ.obj e), a == b.
 \end{coq_example}
 
-Still, no concrete type is in the $EQ$ class.  We amend that by equipping $nat$
+Still, no concrete type is in the \texttt{EQ} class.  We amend that by equipping \texttt{nat}
 with a comparison relation.
 
 \begin{coq_example}
@@ -71,23 +71,23 @@ Check 3 == 3.
 Eval compute in 3 == 4.
 \end{coq_example}
 
-This last test shows that Coq is now not only able to typecheck $3==3$, but
-also that the infix relation was bound to the $nat\_eq$ relation.  This
-relation is selected whenever $==$ is used on terms of type $nat$.  This
-can be read in the line declaring the canonical structure $nat\_EQty$,
-where the first argument to $Pack$ is the key and its second argument
+This last test shows that Coq is now not only able to typecheck \texttt{3==3}, but
+also that the infix relation was bound to the \texttt{nat\_eq} relation.  This
+relation is selected whenever \texttt{==} is used on terms of type \texttt{nat}.  This
+can be read in the line declaring the canonical structure \texttt{nat\_EQty},
+where the first argument to \texttt{Pack} is the key and its second argument
 a group of canonical values associated to the key.  In this case we associate
-to $nat$ only one canonical value (since its class, $nat\_EQcl$ has just one
-member).  The use of the projection $op$ requires its argument to be in
-the class $EQ$, and uses such a member (function) to actually compare
+to \texttt{nat} only one canonical value (since its class, \texttt{nat\_EQcl} has just one
+member).  The use of the projection \texttt{op} requires its argument to be in
+the class \texttt{EQ}, and uses such a member (function) to actually compare
 its arguments.
 
 Similarly, we could equip any other type with a comparison relation, and
-use the $==$ notation on terms of this type.
+use the \texttt{==} notation on terms of this type.
 
 \subsection{Derived Canonical Structures}
 
-We know how to use $==$ on base types, like $nat$, $bool$, $Z$.
+We know how to use \texttt{==} on base types, like \texttt{nat}, \texttt{bool}, \texttt{Z}.
 Here we show how to deal with type constructors, i.e. how to make the
 following example work:
 
@@ -109,18 +109,18 @@ Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b).
 Check forall n m : nat, (3,4) == (n,m).
 \end{coq_example}
 
-Thanks to the $pair\_EQty$ declaration, Coq is able to build a comparison
+Thanks to the \texttt{pair\_EQty} declaration, Coq is able to build a comparison
 relation for pairs whenever it is able to build a comparison relation
 for each component of the pair.  The declaration associates to the key
-$*$ (the type constructor of pairs) the canonical comparison relation
-$pair\_eq$ whenever the type constructor $*$ is applied to two types
-being themselves in the $EQ$ class.
+\texttt{*} (the type constructor of pairs) the canonical comparison relation
+\texttt{pair\_eq} whenever the type constructor \texttt{*} is applied to two types
+being themselves in the \texttt{EQ} class.
 
 \section{Hierarchy of structures}
 
 To get to an interesting example we need another base class to be available.
 We choose the class of types that are equipped with an order relation,
-to which we associate the infix $<=$ notation.
+to which we associate the infix \texttt{<=} notation.
 
 \begin{coq_example}
 Module LE.
@@ -136,7 +136,7 @@ Module LE.
 End LE.
 \end{coq_example}
 
-As before we register a canonical $LE$ class for $nat$.
+As before we register a canonical \texttt{LE} class for \texttt{nat}.
 
 \begin{coq_example}
 Import LE.theory.
@@ -145,7 +145,7 @@ Definition nat_LEcl : LE.class nat := LE.Class nat_le.
 Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.
 \end{coq_example}
 
-And we enable Coq to relate pair of terms with $<=$.
+And we enable Coq to relate pair of terms with \texttt{<=}.
 
 \begin{coq_example}
 Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) :=
@@ -156,7 +156,7 @@ Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type :=
 Check (3,4,5) <= (3,4,5).
 \end{coq_example}
 
-At the current stage we can use $==$ and $<=$ on concrete types,
+At the current stage we can use \texttt{==} and \texttt{<=} on concrete types,
 like tuples of natural numbers, but we can't develop an algebraic
 theory over the types that are equipped with both relations.
 
@@ -166,7 +166,7 @@ Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y.
 Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y.
 \end{coq_example}
 
-We need to define a new class that inherits from both $EQ$ and $LE$.
+We need to define a new class that inherits from both \texttt{EQ} and \texttt{LE}.
 
 \begin{coq_example}
 Module LEQ.
@@ -181,8 +181,8 @@ Module LEQ.
   Arguments Class {T} _ _ _.
 \end{coq_example}
 
-The $mixin$ component of the $LEQ$ class contains all the extra content
-we are adding to $EQ$ and $LE$.  In particular it contains the requirement
+The \texttt{mixin} component of the \texttt{LEQ} class contains all the extra content
+we are adding to \texttt{EQ} and \texttt{LE}.  In particular it contains the requirement
 that the two relations we are combining are compatible.
 
 Unfortunately there is still an obstacle to developing the algebraic theory
@@ -193,12 +193,12 @@ of this new class.
   Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m.
 \end{coq_example}
 
-The problem is that the two classes $LE$ and $LEQ$ are not yet related by
+The problem is that the two classes \texttt{LE} and \texttt{LEQ} are not yet related by
 a subclass relation.  In other words Coq does not see that an object
-of the $LEQ$ class is also an object of the $LE$ class.
+of the \texttt{LEQ} class is also an object of the \texttt{LE} class.
 
 The following two constructions tell Coq how to canonically build
-the $LE.type$ and $EQ.type$ structure given an $LEQ.type$ structure
+the \texttt{LE.type} and \texttt{EQ.type} structure given an \texttt{LEQ.type} structure
 on the same type.
 
 \begin{coq_example}
@@ -209,7 +209,7 @@ on the same type.
     LE.Pack (obj e) (LE_class _ (class_of e)).
   Canonical Structure to_LE.
 \end{coq_example}
-We can now formulate out first theorem on the objects of the $LEQ$ structure.
+We can now formulate out first theorem on the objects of the \texttt{LEQ} structure.
 \begin{coq_example}
   Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y.
    now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. Qed.
@@ -231,8 +231,8 @@ Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
  Fail apply (lele_eq n m). Abort.
 \end{coq_example}
 
-Again one has to tell Coq that the type $nat$ is in the $LEQ$ class, and how
-the type constructor $*$ interacts with the $LEQ$ class.  In the following
+Again one has to tell Coq that the type \texttt{nat} is in the \texttt{LEQ} class, and how
+the type constructor \texttt{*} interacts with the \texttt{LEQ} class.  In the following
 proofs are omitted for brevity.
 
 \begin{coq_example}
@@ -271,8 +271,8 @@ Qed.
 Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2).
 \end{coq_example}
 
-The following script registers an $LEQ$ class for $nat$ and for the
-type constructor $*$.  It also tests that they work as expected.
+The following script registers an \texttt{LEQ} class for \texttt{nat} and for the
+type constructor \texttt{*}.  It also tests that they work as expected.
 
 Unfortunately, these declarations are very verbose.  In the following
 subsection we show how to make these declaration more compact.
@@ -294,9 +294,9 @@ Module Add_instance_attempt.
 End Add_instance_attempt.
 \end{coq_example}
 
-Note that no direct proof of $n <= m -> m <= n -> n == m$ is provided by the
-user for $n$ and $m$ of type $nat * nat$.  What the user provides is a proof of
-this statement for $n$ and $m$ of type $nat$ and a proof that the pair
+Note that no direct proof of \texttt{n <= m -> m <= n -> n == m} is provided by the
+user for \texttt{n} and \texttt{m} of type \texttt{nat * nat}.  What the user provides is a proof of
+this statement for \texttt{n} and \texttt{m} of type \texttt{nat} and a proof that the pair
 constructor preserves this property.  The combination of these two facts is a
 simple form of proof search that Coq performs automatically while inferring
 canonical structures.
@@ -334,7 +334,7 @@ problem, that will in turn require the inference of some canonical
 structures.  They are explained in mode details in~\cite{CSwcu}.
 
 We now have all we need to create a compact ``packager'' to declare
-instances of the $LEQ$ class.
+instances of the \texttt{LEQ} class.
 
 \begin{coq_example}
 Import infrastructure.
@@ -348,17 +348,17 @@ Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) :=
 Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id).
 \end{coq_example}
 
-The object $Pack$ takes a type $T$ (the key) and a mixin $m$.  It infers all
-the other pieces of the class $LEQ$ and declares them as canonical values
-associated to the $T$ key.  All in all, the only new piece of information
-we add in the $LEQ$ class is the mixin, all the rest is already canonical
-for $T$ and hence can be inferred by Coq.
+The object \texttt{Pack} takes a type \texttt{T} (the key) and a mixin \texttt{m}.  It infers all
+the other pieces of the class \texttt{LEQ} and declares them as canonical values
+associated to the \texttt{T} key.  All in all, the only new piece of information
+we add in the \texttt{LEQ} class is the mixin, all the rest is already canonical
+for \texttt{T} and hence can be inferred by Coq.
 
-$Pack$ is a notation, hence it is not type checked at the time of its
+\texttt{Pack} is a notation, hence it is not type checked at the time of its
 declaration.  It will be type checked when it is used, an in that case
-$T$ is going to be a concrete type.  The odd arguments $\_$ and $id$ we
+\texttt{T} is going to be a concrete type.  The odd arguments \texttt{\_} and \texttt{id} we
 pass to the 
-packager represent respectively the classes to be inferred (like $e$, $o$, etc) and a token ($id$) to force their inference.  Again, for all the details the
+packager represent respectively the classes to be inferred (like \texttt{e}, \texttt{o}, etc) and a token (\texttt{id}) to force their inference.  Again, for all the details the
 reader can refer to~\cite{CSwcu}. 
 
 The declaration of canonical instances can now be way more compact:
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index e2827d6bf..7a1189ee3 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4164,6 +4164,12 @@ first-order reasoning, written by Pierre Corbineau.
 It is not restricted to usual logical connectives but
 instead may reason about any first-order class inductive definition.
 
+The default tactic used by \texttt{firstorder} when no rule applies is {\tt
+  auto with *}, it can be reset locally or globally using the {\nobreak
+  {\tt Set Firstorder Solver {\tac}}} \optindex{Firstorder Solver}
+vernacular command and printed using {\nobreak {\tt Print Firstorder
+    Solver}}.
+
 \begin{Variants}
  \item {\tt firstorder {\tac}}
    \tacindex{firstorder {\tac}}
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 341431114..018d73908 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -93,7 +93,7 @@ of monoids).
 
 \begin{coq_example*}
 Polymorphic Definition monoid_monoid : Monoid.
-  refine (@Build_Monoid Monoid unit_monoid _) ; admit.
+  refine (@Build_Monoid Monoid unit_monoid (fun x y => x)).
 Defined.
 \end{coq_example*}
 \begin{coq_example}
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 5aca11ae6..a88c2e20e 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -278,6 +278,7 @@ let make_all_name_different env =
   let avoid = ref (ids_of_named_context (named_context env)) in
   process_rel_context
     (fun (na,c,t) newenv ->
+       let na = named_hd newenv t na in
        let id = next_name_away na !avoid in
        avoid := id::!avoid;
        push_rel (Name id,c,t) newenv)
diff --git a/ide/coq.lang b/ide/coq.lang
index c65432bdb..89f93a705 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -29,7 +29,7 @@
     <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex>
     <define-regex id="dot_sep">\.(\s|\z)</define-regex>
     <define-regex id="bullet">([-+*]+|{)(\s|\z)|}(\s*})*</define-regex>
-    <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion</define-regex>
+    <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion|Universe</define-regex>
     <define-regex id="mult_decl">Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?</define-regex>
     <define-regex id="locality">((Local|Global)\%{space})?</define-regex>
     <define-regex id="begin_proof">Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property</define-regex>
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 2387d65c3..c6d314947 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -669,7 +669,10 @@ object(self)
       push_info "Coq is undoing" in
     let conclusion () =
       pop_info ();
-      if move_insert then buffer#place_cursor ~where:self#get_start_of_input;
+      if move_insert then begin
+        buffer#place_cursor ~where:self#get_start_of_input;
+        script#recenter_insert;
+      end;
       let start = self#get_start_of_input in
       let stop = self#get_end_of_input in
       Minilib.log(Printf.sprintf "cleanup tags %d %d" start#offset stop#offset);
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index dc52ea9aa..94f9c9a36 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -185,13 +185,15 @@ let process_goal sigma g =
   let ccl =
     let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
     string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in
-  let process_hyp d =
+  let process_hyp d (env,l) =
     let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in
-    (string_of_ppcmds (pr_var_list_decl min_env sigma d)) in
-  let hyps =
-    List.map process_hyp
-      (Termops.compact_named_context_reverse (Environ.named_context env)) in
-  { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
+    let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in
+      (List.fold_right Environ.push_named d' env,
+       (string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in
+  let (_env, hyps) =
+    Context.fold_named_list_context process_hyp
+      (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
+  { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
 let export_pre_goals pgs =
   {
diff --git a/interp/notation.ml b/interp/notation.ml
index 0b5791d32..d18b804bf 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -796,8 +796,8 @@ let pr_scope_classes sc =
   let l = classes_of_scope sc in
   match l with
   | [] -> mt ()
-  | _ :: l ->
-    let opt_s = match l with [] -> mt () | _ -> str "es" in
+  | _ :: ll ->
+    let opt_s = match ll with [] -> mt () | _ -> str "es" in
     hov 0 (str "Bound to class" ++ opt_s ++
       spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl()
 
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index c1c19a757..561c66b42 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -14,7 +14,10 @@ open Context
    declarations. This includes global constants/axioms, mutual
    inductive definitions, modules and module types *)
 
-type engagement = ImpredicativeSet
+type set_predicativity = ImpredicativeSet | PredicativeSet
+type type_hierarchy = TypeInType | StratifiedType
+
+type engagement = set_predicativity * type_hierarchy
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a79abbb7e..30b28177c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,11 +46,14 @@ let empty_env = empty_env
 
 let engagement env = env.env_stratification.env_engagement
 
-let type_in_type env = env.env_stratification.env_type_in_type
-
 let is_impredicative_set env = 
-  match engagement env with
-  | Some ImpredicativeSet -> true
+  match fst (engagement env) with
+  | ImpredicativeSet -> true
+  | _ -> false
+
+let type_in_type env =
+  match snd (engagement env) with
+  | TypeInType -> true
   | _ -> false
 
 let universes env = env.env_stratification.env_universes
@@ -191,11 +194,7 @@ let check_constraints c env =
 
 let set_engagement c env = (* Unsafe *)
   { env with env_stratification =
-    { env.env_stratification with env_engagement = Some c } }
-
-let set_type_in_type env =
-  { env with env_stratification =
-    { env.env_stratification with env_type_in_type = true } }
+    { env.env_stratification with env_engagement = c } }
 
 let push_constraints_to_env (_,univs) env =
   add_constraints univs env
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ede356e69..4ad0327fc 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -50,10 +50,9 @@ val opaque_tables : env -> Opaqueproof.opaquetab
 val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
 
 
-val engagement    : env -> engagement option
+val engagement    : env -> engagement
 val is_impredicative_set : env -> bool
-
-val type_in_type  : env -> bool
+val type_in_type : env -> bool
 
 (** is the local context empty *)
 val empty_context : env -> bool
@@ -215,8 +214,6 @@ val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
 val set_engagement : engagement -> env -> env
 
-val set_type_in_type : env -> env
-
 (** {6 Sets of referred section variables }
    [global_vars_set env c] returns the list of [id]'s occurring either
    directly as [Var id] in [c] or indirectly as a section variable
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 86fb1b64c..d22abff10 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -182,14 +182,12 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        begin match engagement env with
-        | Some ImpredicativeSet ->
+        if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        | _ ->
+        else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (Universe.sup Universe.type0 u1)
-        end
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Pos,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
     (* Product rule (Prop,Type_i,Type_i) *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 92e121402..3c137ee92 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -178,38 +178,21 @@ let cumulate_arity_large_levels env sign =
     sign (Universe.type0m,env))
 
 let is_impredicative env u =
-  is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet)
+  is_type0m_univ u || (is_type0_univ u && is_impredicative_set env)
 
+(* Returns the list [x_1, ..., x_n] of levels contributing to template
+   polymorphism. The elements x_k is None if the k-th parameter (starting
+   from the most recent and ignoring let-definitions) is not contributing 
+   or is Some u_k if its level is u_k and is contributing. *)
 let param_ccls params =
-  let has_some_univ u = function
-    | Some v when Univ.Level.equal u v -> true
-    | _ -> false
+  let fold acc = function (_, None, p) -> 
+      (let c = strip_prod_assum p in
+      match kind_of_term c with
+        | Sort (Type u) -> Univ.Universe.level u
+        | _ -> None) :: acc
+    | _ -> acc 
   in
-  let remove_some_univ u = function
-    | Some v when Univ.Level.equal u v -> None
-    | x -> x
-  in
-  let fold l (_, b, p) = match b with
-  | None ->
-    (* Parameter contributes to polymorphism only if explicit Type *)
-    let c = strip_prod_assum p in
-    (* Add Type levels to the ordered list of parameters contributing to *)
-    (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
-    begin match kind_of_term c with
-    | Sort (Type u) ->
-      (match Univ.Universe.level u with
-      | Some u ->
-	if List.exists (has_some_univ u) l then
-          None :: List.map (remove_some_univ u) l
-	else
-          Some u :: l
-      | None -> None :: l)
-    | _ ->
-      None :: l
-    end
-  | _ -> l
-  in
-    List.fold_left fold [] params
+  List.fold_left fold [] params
 
 (* Type-check an inductive definition. Does not check positivity
    conditions. *)
@@ -705,10 +688,28 @@ exception UndefinableExpansion
     build an expansion function.
     The term built is expecting to be substituted first by 
     a substitution of the form [params, x : ind params] *)
-let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
-    mind_consnrealdecls mind_consnrealargs ctx =
+let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
+    mind_consnrealdecls mind_consnrealargs paramslet ctx =
   let mp, dp, l = repr_mind kn in
-  let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in
+  (** We build a substitution smashing the lets in the record parameters so
+      that typechecking projections requires just a substitution and not
+      matching with a parameter context. *)
+  let indty, paramsletsubst =
+    let subst, inst = 
+      List.fold_right
+	(fun (na, b, t) (subst, inst) ->
+	 match b with
+	 | None -> (mkRel 1 :: List.map (lift 1) subst,
+		   mkRel 1 :: List.map (lift 1) inst)
+	 | Some b -> (substl subst b) :: subst, List.map (lift 1) inst)
+	paramslet ([], [])
+    in
+    let subst = (* For the record parameter: *)
+      mkRel 1 :: List.map (lift 1) subst
+    in
+    let ty = mkApp (mkIndU indu, CArray.rev_of_list inst) in
+      ty, subst
+  in
   let ci = 
     let print_info =
       { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
@@ -721,34 +722,39 @@ let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
   let len = List.length ctx in
   let x = Name x in
   let compat_body ccl i = 
-    (* [ccl] is defined in context [params;x:rp] *)
-    (* [ccl'] is defined in context [params;x:rp;x:rp] *)
+    (* [ccl] is defined in context [params;x:indty] *)
+    (* [ccl'] is defined in context [params;x:indty;x:indty] *)
     let ccl' = liftn 1 2 ccl in
-    let p = mkLambda (x, lift 1 rp, ccl') in
+    let p = mkLambda (x, lift 1 indty, ccl') in
     let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
     let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
-      it_mkLambda_or_LetIn (mkLambda (x,rp,body)) params
+      it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
   in
-  let projections (na, b, t) (i, j, kns, pbs, subst) =
+  let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) =
     match b with
-    | Some c -> (i, j+1, kns, pbs, substl subst c :: subst)
+    | Some c -> (i, j+1, kns, pbs, substl subst c :: subst,
+		substl letsubst c :: subst)
     | None ->
       match na with
       | Name id ->
 	let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
+	let projty = substl letsubst (liftn 1 j t) in
 	let ty = substl subst (liftn 1 j t) in
 	let term = mkProj (Projection.make kn true, mkRel 1) in
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
 	let compat = compat_body ty (j - 1) in
-	let etab = it_mkLambda_or_LetIn (mkLambda (x, rp, term)) params in
-	let etat = it_mkProd_or_LetIn (mkProd (x, rp, ty)) params in
+	let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
+	let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
 	let body = { proj_ind = fst ind; proj_npars = nparamargs;
-		     proj_arg = i; proj_type = ty; proj_eta = etab, etat; 
+		     proj_arg = i; proj_type = projty; proj_eta = etab, etat; 
 		     proj_body = compat } in
-	  (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: subst)
+	  (i + 1, j + 1, kn :: kns, body :: pbs,
+	   fterm :: subst, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
   in
-  let (_, _, kns, pbs, subst) = List.fold_right projections ctx (0, 1, [], [], []) in
+  let (_, _, kns, pbs, subst, letsubst) =
+    List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
+  in
     Array.of_list (List.rev kns),
     Array.of_list (List.rev pbs)
 
@@ -834,12 +840,12 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 	else Univ.Instance.empty 
       in
       let indsp = ((kn, 0), u) in
-      let rctx, _ = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
+      let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
 	(try 
-	   let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in
+	   let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
 	   let kns, projs = 
 	     compute_projections indsp pkt.mind_typename rid nparamargs params
-	       pkt.mind_consnrealdecls pkt.mind_consnrealargs fields
+	       pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
 	   in Some (Some (rid, kns, projs))
 	 with UndefinableExpansion -> Some None)
     | Some _ -> Some None
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7774e52e9..01acdce5c 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -43,5 +43,5 @@ val is_indices_matter : unit -> bool
 
 val compute_projections : pinductive -> Id.t -> Id.t ->
   int -> Context.rel_context -> int array -> int array -> 
-  Context.rel_context -> 
+  Context.rel_context -> Context.rel_context -> 
   (constant array * projection_body array)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 4c1614bac..87c139f48 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -73,7 +73,7 @@ let constructor_instantiate mind u mib c =
   let s = ind_subst mind mib u in
     substl s (subst_instance_constr u c)
 
-let instantiate_params full t args sign =
+let instantiate_params full t u args sign =
   let fail () =
     anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
   let (rem_args, subs, ty) =
@@ -81,7 +81,8 @@ let instantiate_params full t args sign =
       (fun (_,copt,_) (largs,subs,ty) ->
         match (copt, largs, kind_of_term ty) with
           | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
-          | (Some b,_,LetIn(_,_,_,t))    -> (largs, (substl subs b)::subs, t)
+          | (Some b,_,LetIn(_,_,_,t))    ->
+	     (largs, (substl subs (subst_instance_constr u b))::subs, t)
 	  | (_,[],_)                -> if full then fail() else ([], subs, ty)
 	  | _                       -> fail ())
       sign
@@ -92,15 +93,13 @@ let instantiate_params full t args sign =
 
 let full_inductive_instantiate mib u params sign =
   let dummy = prop_sort in
-  let t = mkArity (sign,dummy) in
-  let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
-    Vars.subst_instance_context u ar
-
-let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
-  let inst_ind = constructor_instantiate mind u mib in
-  (fun t ->
-    instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
+  let t = mkArity (Vars.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 =
+  let inst_ind = constructor_instantiate mind u mib t in
+   instantiate_params true inst_ind u params mib.mind_params_ctxt
+		      
 (************************************************************************)
 (************************************************************************)
 
@@ -134,46 +133,60 @@ let sort_as_univ = function
 
 (* Template polymorphism *)
 
+(* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
+(* in the domain or add [u |-> sup x su] if [u] is already mapped *)
+(* to [x]. *)
 let cons_subst u su subst =
-  Univ.LMap.add u su subst
+  try
+    Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+  with Not_found -> Univ.LMap.add u su subst
+
+(* remember_subst updates the mapping [u |-> x] by [u |-> sup x u] *)
+(* if it is presents and returns the substitution unchanged if not.*)
+let remember_subst u subst =
+  try
+    let su = Universe.make u in
+    Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+  with Not_found -> subst
 
 (* Bind expected levels of parameters to actual levels *)
 (* Propagate the new levels in the signature *)
-let rec make_subst env = function
-  | (_,Some _,_ as t)::sign, exp, args ->
-      let ctx,subst = make_subst env (sign, exp, args) in
-      t::ctx, subst
-  | d::sign, None::exp, args ->
-      let args = match args with _::args -> args | [] -> [] in
-      let ctx,subst = make_subst env (sign, exp, args) in
-      d::ctx, subst
-  | d::sign, Some u::exp, a::args ->
-      (* We recover the level of the argument, but we don't change the *)
-      (* level in the corresponding type in the arity; this level in the *)
-      (* arity is a global level which, at typing time, will be enforce *)
-      (* to be greater than the level of the argument; this is probably *)
-      (* a useless extra constraint *)
-      let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
-      let ctx,subst = make_subst env (sign, exp, args) in
-      d::ctx, cons_subst u s subst
-  | (na,None,t as d)::sign, Some u::exp, [] ->
-      (* No more argument here: we instantiate the type with a fresh level *)
-      (* which is first propagated to the corresponding premise in the arity *)
-      (* (actualize_decl_level), then to the conclusion of the arity (via *)
-      (* the substitution) *)
-      let ctx,subst = make_subst env (sign, exp, []) in
-	d::ctx, subst
-  | sign, [], _ ->
-      (* Uniform parameters are exhausted *)
-      sign, Univ.LMap.empty
-  | [], _, _ ->
-      assert false
+let rec make_subst env =
+  let rec make subst = function
+    | (_,Some _,_)::sign, exp, args ->
+        make subst (sign, exp, args)
+    | d::sign, None::exp, args ->
+        let args = match args with _::args -> args | [] -> [] in
+        make subst (sign, exp, args)
+    | d::sign, Some u::exp, a::args ->
+        (* We recover the level of the argument, but we don't change the *)
+        (* level in the corresponding type in the arity; this level in the *)
+        (* arity is a global level which, at typing time, will be enforce *)
+        (* to be greater than the level of the argument; this is probably *)
+        (* a useless extra constraint *)
+        let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
+        make (cons_subst u s subst) (sign, exp, args)
+    | (na,None,t)::sign, Some u::exp, [] ->
+        (* No more argument here: we add the remaining universes to the *)
+        (* substitution (when [u] is distinct from all other universes in the *)
+        (* template, it is identity substitution  otherwise (ie. when u is *)
+        (* already in the domain of the substitution) [remember_subst] will *)
+        (* update its image [x] by [sup x u] in order not to forget the *)
+        (* dependency in [u] that remains to be fullfilled. *)
+        make (remember_subst u subst) (sign, exp, [])
+    | sign, [], _ ->
+        (* Uniform parameters are exhausted *)
+        subst
+    | [], _, _ ->
+        assert false
+  in
+  make Univ.LMap.empty
 
 exception SingletonInductiveBecomesProp of Id.t
 
 let instantiate_universes env ctx ar argsorts =
   let args = Array.to_list argsorts in
-  let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
+  let subst = make_subst env (ctx,ar.template_param_levels,args) in
   let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
@@ -331,13 +344,13 @@ let is_correct_arity env c pj ind specif params =
       | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
 	 let env' = push_rel (na1,None,a1) env in
 	 let ksort = match kind_of_term (whd_betadeltaiota env' a2) with
-       | Sort s -> family_of_sort s
-       | _ -> raise (LocalArity None) in
+	 | Sort s -> family_of_sort s
+	 | _ -> raise (LocalArity None) in
 	 let dep_ind = build_dependent_inductive ind specif params in
 	 let _ =
            try conv env a1 dep_ind
            with NotConvertible -> raise (LocalArity None) in
-	 check_allowed_sort ksort specif
+	   check_allowed_sort ksort specif
       | _, (_,Some _,_ as d)::ar' ->
 	  srec (push_rel d env) (lift 1 pt') ar'
       | _ ->
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 26dd45f5f..4f20e5f62 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -307,7 +307,9 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
     { res_mtb with
       mod_mp = mp;
       mod_expr = impl;
-      mod_constraints = cst +++ cst' }
+      (** cst from module body typing, cst' from subtyping, 
+          and constraints from module type. *)
+      mod_constraints = cst +++ cst' +++ res_mtb.mod_constraints }
 
 let translate_module env mp inl = function
   |MType (params,ty) ->
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index f56b6f83e..90c437bbf 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -195,7 +195,11 @@ module HashtblSymbol = Hashtbl.Make(HashedTypeSymbol)
 
 let symb_tbl = HashtblSymbol.create 211
 
-let clear_symb_tbl () = HashtblSymbol.clear symb_tbl
+let clear_symbols () = HashtblSymbol.clear symb_tbl
+
+type symbols = symbol array
+
+let empty_symbols = [||]
 
 let get_value tbl i =
   match tbl.(i) with
@@ -250,7 +254,7 @@ let push_symbol x =
 
 let symbols_tbl_name = Ginternal "symbols_tbl"
 
-let get_symbols_tbl () =
+let get_symbols () =
   let tbl = Array.make (HashtblSymbol.length symb_tbl) dummy_symb in
   HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl
 
@@ -2058,7 +2062,7 @@ let mk_internal_let s code =
 
 (* ML Code for conversion function *)
 let mk_conv_code env sigma prefix t1 t2 =
-  clear_symb_tbl ();
+  clear_symbols ();
   clear_global_tbl ();
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
@@ -2080,12 +2084,12 @@ let mk_conv_code env sigma prefix t1 t2 =
   let setref2 = Glet(Ginternal "_", MLsetref("rt2",g2)) in
   let gl = List.rev (setref2 :: setref1 :: t2 :: t1 :: gl) in
   let header = Glet(Ginternal "symbols_tbl",
-    MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+    MLapp (MLglobal (Ginternal "get_symbols"),
       [|MLglobal (Ginternal "()")|])) in
   header::gl, (mind_updates, const_updates)
 
 let mk_norm_code env sigma prefix t =
-  clear_symb_tbl ();
+  clear_symbols ();
   clear_global_tbl ();
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
@@ -2098,14 +2102,14 @@ let mk_norm_code env sigma prefix t =
   let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in
   let gl = List.rev (setref :: t1 :: gl) in
   let header = Glet(Ginternal "symbols_tbl",
-    MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+    MLapp (MLglobal (Ginternal "get_symbols"),
       [|MLglobal (Ginternal "()")|])) in
   header::gl, (mind_updates, const_updates)
 
 let mk_library_header dir =
   let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in
   [Glet(Ginternal "symbols_tbl",
-    MLapp (MLglobal (Ginternal "get_library_symbols_tbl"),
+    MLapp (MLglobal (Ginternal "get_library_native_symbols"),
     [|MLglobal (Ginternal libname)|]))]
 
 let update_location (r,v) = r := v
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 893db92dd..5d4c9e1e2 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -22,29 +22,33 @@ val pp_global : Format.formatter -> global -> unit
 
 val mk_open : string -> global
 
+(* Precomputed values for a compilation unit *)
 type symbol
+type symbols
 
-val clear_symb_tbl : unit -> unit
+val empty_symbols : symbols
 
-val get_value : symbol array -> int -> Nativevalues.t
+val clear_symbols : unit -> unit
 
-val get_sort : symbol array -> int -> sorts
+val get_value : symbols -> int -> Nativevalues.t
 
-val get_name : symbol array -> int -> name
+val get_sort : symbols -> int -> sorts
 
-val get_const : symbol array -> int -> constant
+val get_name : symbols -> int -> name
 
-val get_match : symbol array -> int -> Nativevalues.annot_sw
+val get_const : symbols -> int -> constant
 
-val get_ind : symbol array -> int -> inductive
+val get_match : symbols -> int -> Nativevalues.annot_sw
 
-val get_meta : symbol array -> int -> metavariable
+val get_ind : symbols -> int -> inductive
 
-val get_evar : symbol array -> int -> existential
+val get_meta : symbols -> int -> metavariable
 
-val get_level : symbol array -> int -> Univ.Level.t
+val get_evar : symbols -> int -> existential
 
-val get_symbols_tbl : unit -> symbol array
+val get_level : symbols -> int -> Univ.Level.t
+
+val get_symbols : unit -> symbols
 
 type code_location_update
 type code_location_updates
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index ce9e4e2b0..331598d85 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -107,9 +107,11 @@ let call_linker ?(fatal=true) prefix f upds =
   rt1 := dummy_value ();
   rt2 := dummy_value ();
   if not (Sys.file_exists f) then
-    let msg = "Cannot find native compiler file " ^ f in
-    if fatal then Errors.error msg
-    else Pp.msg_warning (Pp.str msg)
+    begin
+      let msg = "Cannot find native compiler file " ^ f in
+      if fatal then Errors.error msg
+      else if !Flags.debug then Pp.msg_debug (Pp.str msg)
+    end
   else
   (try
     if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
@@ -118,7 +120,7 @@ let call_linker ?(fatal=true) prefix f upds =
      let exn = Errors.push exn in
      let msg = "Dynlink error, " ^ Dynlink.error_message e in
      if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
-     else Pp.msg_warning (Pp.str msg));
+     else if !Flags.debug then Pp.msg_debug (Pp.str msg));
   match upds with Some upds -> update_locations upds | _ -> ()
 
 let link_library ~prefix ~dirname ~basename =
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 0b8662ff0..443cd8c2a 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -62,12 +62,12 @@ let dump_library mp dp env mod_expr =
       let prefix = mod_uid_of_dirpath dp ^ "." in
       let t0 = Sys.time () in
       clear_global_tbl ();
-      clear_symb_tbl ();
+      clear_symbols ();
       let mlcode =
         List.fold_left (translate_field prefix mp env) [] struc
       in
       let t1 = Sys.time () in
       let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in
       let mlcode = add_header_comment (List.rev mlcode) time_info in
-      mlcode, get_symbols_tbl ()
+      mlcode, get_symbols ()
   | _ -> assert false
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index a66fb715d..29368d140 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -14,4 +14,4 @@ open Nativecode
 compiler *)
 
 val dump_library : module_path -> dir_path -> env -> module_signature ->
-  global list * symbol array
+  global list * symbols
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 557ed3d7d..5f3f559a2 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -46,8 +46,7 @@ type globals = {
 
 type stratification = {
   env_universes : universes;
-  env_engagement : engagement option;
-  env_type_in_type : bool
+  env_engagement : engagement
 }
 
 type val_kind =
@@ -95,8 +94,7 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = initial_universes;
-    env_engagement = None;
-    env_type_in_type = false};
+    env_engagement = (PredicativeSet,StratifiedType) };
   env_conv_oracle = Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge;
   indirect_pterms = Opaqueproof.empty_opaquetab }
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 03ac41b45..0ce0bed23 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -33,8 +33,7 @@ type globals = {
 
 type stratification = {
   env_universes : universes;
-  env_engagement : engagement option;
-  env_type_in_type : bool
+  env_engagement : engagement
 }
 
 type lazy_val
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d9adca0c9..907ad2a1d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -125,7 +125,8 @@ type safe_environment =
     type_in_type : bool;
     required : vodigest DPMap.t;
     loads : (module_path * module_body) list;
-    local_retroknowledge : Retroknowledge.action list }
+    local_retroknowledge : Retroknowledge.action list;
+    native_symbols : Nativecode.symbols DPMap.t }
 
 and modvariant =
   | NONE
@@ -154,7 +155,8 @@ let empty_environment =
     type_in_type = false;
     required = DPMap.empty;
     loads = [];
-    local_retroknowledge = [] }
+    local_retroknowledge = [];
+    native_symbols = DPMap.empty }
 
 let is_initial senv =
   match senv.revstruct, senv.modvariant with
@@ -182,16 +184,20 @@ let set_engagement c senv =
 
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
-let check_engagement env c =
-  match Environ.engagement env, c with
-  | None, Some ImpredicativeSet ->
-    Errors.error "Needs option -impredicative-set."
-  | _ -> ()
-
-let set_type_in_type senv = 
-  { senv with
-    env = Environ.set_type_in_type senv.env;
-    type_in_type = true }
+let check_engagement env (expected_impredicative_set,expected_type_in_type) =
+  let impredicative_set,type_in_type = Environ.engagement env in
+  begin
+    match impredicative_set, expected_impredicative_set with
+    | PredicativeSet, ImpredicativeSet ->
+        Errors.error "Needs option -impredicative-set."
+    | _ -> ()
+  end;
+  begin
+    match type_in_type, expected_type_in_type with
+    | StratifiedType, TypeInType ->
+        Errors.error "Needs option -type-in-type."
+    | _ -> ()
+  end
 
 (** {6 Stm machinery } *)
 
@@ -623,7 +629,8 @@ let propagate_senv newdef newenv newresolver senv oldsenv =
     required = senv.required;
     loads = senv.loads@oldsenv.loads;
     local_retroknowledge =
-            senv.local_retroknowledge@oldsenv.local_retroknowledge }
+            senv.local_retroknowledge@oldsenv.local_retroknowledge;
+    native_symbols = senv.native_symbols}
 
 let end_module l restype senv =
   let mp = senv.modpath in
@@ -731,12 +738,15 @@ type compiled_library = {
   comp_name : DirPath.t;
   comp_mod : module_body;
   comp_deps : library_info array;
-  comp_enga : engagement option;
-  comp_natsymbs : Nativecode.symbol array
+  comp_enga : engagement;
+  comp_natsymbs : Nativecode.symbols
 }
 
 type native_library = Nativecode.global list
 
+let get_library_native_symbols senv dir =
+  DPMap.find dir senv.native_symbols
+
 (** FIXME: MS: remove?*)
 let current_modpath senv = senv.modpath
 let current_dirpath senv = Names.ModPath.dp (current_modpath senv)
@@ -773,17 +783,17 @@ let export ?except senv dir =
       mod_retroknowledge = senv.local_retroknowledge
     }
   in
-  let ast, values =
+  let ast, symbols =
     if !Flags.native_compiler then
       Nativelibrary.dump_library mp dir senv.env str
-    else [], [||]
+    else [], Nativecode.empty_symbols
   in
   let lib = {
     comp_name = dir;
     comp_mod = mb;
     comp_deps = Array.of_list (DPMap.bindings senv.required);
     comp_enga = Environ.engagement senv.env;
-    comp_natsymbs = values }
+    comp_natsymbs = symbols }
   in
   mp, lib, ast
 
@@ -796,7 +806,7 @@ let import lib cst vodigest senv =
   let mb = lib.comp_mod in
   let env = Environ.add_constraints mb.mod_constraints senv.env in
   let env = Environ.push_context_set cst env in
-  (mp, lib.comp_natsymbs),
+  mp,
   { senv with
     env =
       (let linkinfo =
@@ -805,7 +815,8 @@ let import lib cst vodigest senv =
        Modops.add_linked_module mb linkinfo env);
     modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
     required = DPMap.add lib.comp_name vodigest senv.required;
-    loads = (mp,mb)::senv.loads }
+    loads = (mp,mb)::senv.loads;
+    native_symbols = DPMap.add lib.comp_name lib.comp_natsymbs senv.native_symbols }
 
 (** {6 Safe typing } *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index a57fb108c..2b4324b96 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -99,12 +99,9 @@ val add_constraints :
 (* (\** Generator of universes *\) *)
 (* val next_universe : int safe_transformer *)
 
-(** Setting the strongly constructive or classical logical engagement *)
+(** Setting the type theory flavor *)
 val set_engagement : Declarations.engagement -> safe_transformer0
 
-(** Collapsing the type hierarchy *)
-val set_type_in_type : safe_transformer0
-
 (** {6 Interactive module functions } *)
 
 val start_module : Label.t -> module_path safe_transformer
@@ -137,6 +134,8 @@ type compiled_library
 
 type native_library = Nativecode.global list
 
+val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols
+
 val start_library : DirPath.t -> module_path safe_transformer
 
 val export :
@@ -146,7 +145,7 @@ val export :
 
 (* Constraints are non empty iff the file is a vi2vo *)
 val import : compiled_library -> Univ.universe_context_set -> vodigest ->
-  (module_path * Nativecode.symbol array) safe_transformer
+  module_path safe_transformer
 
 (** {6 Safe typing judgments } *)
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 48dbacf1a..fe82d85d5 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -252,14 +252,12 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        begin match engagement env with
-        | Some ImpredicativeSet ->
+        if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        | _ ->
+        else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (Universe.sup Universe.type0 u1)
-        end
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Pos,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
     (* Product rule (Prop,Type_i,Type_i) *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1d82be63b..336cdb653 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -577,7 +577,7 @@ struct
   let is_type0m x = equal type0m x
   let is_type0 x = equal type0 x
 
-  (* Returns the formal universe that lies juste above the universe variable u.
+  (* Returns the formal universe that lies just above the universe variable u.
      Used to type the sort u. *)
   let super l = 
     if is_small l then type1
diff --git a/library/declaremods.ml b/library/declaremods.ml
index a82f5260b..f66656d09 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -845,10 +845,6 @@ type library_objects = Lib.lib_objects * Lib.lib_objects
 
 (** For the native compiler, we cache the library values *)
 
-type library_values = Nativecode.symbol array
-let library_values =
-  Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES"
-
 let register_library dir cenv (objs:library_objects) digest univ =
   let mp = MPfile dir in
   let () =
@@ -857,15 +853,15 @@ let register_library dir cenv (objs:library_objects) digest univ =
       ignore(Global.lookup_module mp);
     with Not_found ->
       (* If not, let's do it now ... *)
-      let mp', values = Global.import cenv univ digest in
+      let mp' = Global.import cenv univ digest in
       if not (ModPath.equal mp mp') then
         anomaly (Pp.str "Unexpected disk module name");
-      library_values := Dirmap.add dir values !library_values
   in
   let sobjs,keepobjs = objs in
   do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs
 
-let get_library_symbols_tbl dir = Dirmap.find dir !library_values
+let get_library_native_symbols dir =
+  Safe_typing.get_library_native_symbols (Global.safe_env ()) dir
 
 let start_library dir =
   let mp = Global.start_library dir in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index c3578ec42..319d168d0 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -75,7 +75,7 @@ val register_library :
   Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest ->
   Univ.universe_context_set -> unit
 
-val get_library_symbols_tbl : library_name -> Nativecode.symbol array
+val get_library_native_symbols : library_name -> Nativecode.symbols
 
 val start_library : library_name -> unit
 
diff --git a/library/global.ml b/library/global.ml
index 49fa2ef28..0419799b6 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -84,7 +84,6 @@ let push_context_set c = globalize0 (Safe_typing.push_context_set c)
 let push_context c = globalize0 (Safe_typing.push_context c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
-let set_type_in_type () = globalize0 (Safe_typing.set_type_in_type)
 let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
 let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
diff --git a/library/global.mli b/library/global.mli
index 248e1f86d..363bb5789 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -27,7 +27,6 @@ val named_context : unit -> Context.named_context
 
 (** Changing the (im)predicativity of the system *)
 val set_engagement : Declarations.engagement -> unit
-val set_type_in_type : unit -> unit
 
 (** Variables, Local definitions, constants, inductive types *)
 
@@ -102,7 +101,7 @@ val export : ?except:Future.UUIDSet.t -> DirPath.t ->
   module_path * Safe_typing.compiled_library * Safe_typing.native_library
 val import :
   Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest ->
-  module_path * Nativecode.symbol array
+  module_path
 
 (** {6 Misc } *)
 
diff --git a/library/library.ml b/library/library.ml
index a8fbe0841..45fce1c26 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -169,8 +169,9 @@ let register_loaded_library m =
     let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
     let f = prefix ^ "cmo" in
     let f = Dynlink.adapt_filename f in
-    if !Flags.native_compiler then
-      Nativelib.link_library ~prefix ~dirname ~basename:f
+    (* This will not produce errors or warnings if the native compiler was
+       not enabled *)
+    Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
     | [] -> link m; [libname]
diff --git a/library/nameops.ml b/library/nameops.ml
index 02b085a7a..3a23ab97d 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -136,6 +136,11 @@ let name_fold_map f e = function
   | Name id -> let (e,id) = f e id in (e,Name id)
   | Anonymous -> e,Anonymous
 
+let name_max na1 na2 =
+  match na1 with
+  | Name _ -> na1
+  | Anonymous -> na2
+
 let pr_lab l = str (Label.to_string l)
 
 let default_library = Names.DirPath.initial (* = ["Top"] *)
diff --git a/library/nameops.mli b/library/nameops.mli
index 23432ae2f..de1f99fe0 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -34,7 +34,7 @@ val name_iter : (Id.t -> unit) -> Name.t -> unit
 val name_cons : Name.t -> Id.t list -> Id.t list
 val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
 val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
-
+val name_max : Name.t -> Name.t -> Name.t
 
 val pr_lab : Label.t -> Pp.std_ppcmds
 
diff --git a/library/universes.ml b/library/universes.ml
index a3926bc6f..1c8a5ad77 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -723,7 +723,10 @@ let pr_constraints_map cmap =
       prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ fnl ()
     ++ acc)
     cmap (mt ())
-	
+
+let remove_alg l (ctx, us, algs, insts, cstrs) =
+  (ctx, us, LSet.remove l algs, insts, cstrs)
+    
 let minimize_univ_variables ctx us algs left right cstrs =
   let left, lbounds = 
     Univ.LMap.fold (fun r lower (left, lbounds as acc)  ->
@@ -767,8 +770,8 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	     if not (Level.equal l u) then
 	       (* Should check that u does not 
   	          have upper constraints that are not already in right *)
-	       let acc' = (ctx', us, LSet.remove l algs, insts, cstrs) in
-		 instantiate_with_lbound u lbound false false acc
+	       let acc' = remove_alg l acc in
+		 instantiate_with_lbound u lbound false false acc'
 	     else acc, (true, false, lbound)
 	| None -> 
 	  try 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index c421b4505..e2bb2d1a0 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -78,9 +78,9 @@ val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_univer
 
 (** {6 Lookup functions for coercion paths } *)
 
-val lookup_path_between_class : cl_index * cl_index -> inheritance_path
-(** @raise Not_found when no such path exists *)
+(** @raise Not_found in the following functions when no path exists *)
 
+val lookup_path_between_class : cl_index * cl_index -> inheritance_path
 val lookup_path_between : env -> evar_map -> types * types ->
       types * types * inheritance_path
 val lookup_path_to_fun_from : env -> evar_map -> types ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6765ca130..e61e52c17 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -345,7 +345,7 @@ let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
     ~filter:Typeclasses.no_goals ~split:false ~fail:false env evd
 
-(* appliquer le chemin de coercions p à hj *)
+(* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
 let apply_coercion env sigma p hj typ_cl =
   try
     let j,t,evd = 
@@ -367,7 +367,8 @@ let apply_coercion env sigma p hj typ_cl =
   with NoCoercion as e -> raise e
   | e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion")
 
-let inh_app_fun env evd j =
+(* Try to coerce to a funclass; raise NoCoercion if not possible *)
+let inh_app_fun_core env evd j =
   let t = whd_betadeltaiota env evd j.uj_type in
     match kind_of_term t with
     | Prod (_,_,_) -> (evd,j)
@@ -387,16 +388,17 @@ let inh_app_fun env evd j =
 	      (!evdref, res)
 	  with NoSubtacCoercion | NoCoercion ->
 	    (evd,j)
-          else (evd, j)
+          else raise NoCoercion
 
+(* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
 let inh_app_fun resolve_tc env evd j =
-  try inh_app_fun env evd j
+  try inh_app_fun_core env evd j
   with
-  | Not_found when not resolve_tc 
+  | NoCoercion when not resolve_tc
     || not !use_typeclasses_for_conversion -> (evd, j)
-  | Not_found ->
-    try inh_app_fun env (saturate_evd env evd) j
-    with Not_found -> (evd, j)
+  | NoCoercion ->
+    try inh_app_fun_core env (saturate_evd env evd) j
+    with NoCoercion -> (evd, j)
 
 let inh_tosort_force loc env evd j =
   try
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 97b1b1645..bb07bf056 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -552,13 +552,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
     | MaybeFlexible v1, MaybeFlexible v2 -> begin
         match kind_of_term term1, kind_of_term term2 with
-        | LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) ->
+        | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) ->
         let f1 i =
           ise_and i
 	    [(fun i -> evar_conv_x ts env i CONV b1 b2);
 	     (fun i ->
 	       let b = nf_evar i b1 in
 	       let t = nf_evar i t1 in
+               let na = Nameops.name_max na1 na2 in
 	       evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2);
 	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
 	and f2 i =
@@ -666,13 +667,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     end
 
     | Rigid, Rigid when isLambda term1 && isLambda term2 ->
-        let (na,c1,c'1) = destLambda term1 in
-        let (_,c2,c'2) = destLambda term2 in
+        let (na1,c1,c'1) = destLambda term1 in
+        let (na2,c2,c'2) = destLambda term2 in
         assert app_empty;
         ise_and evd
           [(fun i -> evar_conv_x ts env i CONV c1 c2);
            (fun i ->
 	     let c = nf_evar i c1 in
+             let na = Nameops.name_max na1 na2 in
 	     evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)]
 
     | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
@@ -726,12 +728,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
                UnifFailure (evd,UnifUnivInconsistency p)
 	     | e when Errors.noncritical e -> UnifFailure (evd,NotSameHead))
 
-	| Prod (n,c1,c'1), Prod (_,c2,c'2) when app_empty ->
+	| Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty ->
             ise_and evd
               [(fun i -> evar_conv_x ts env i CONV c1 c2);
                (fun i ->
  	         let c = nf_evar i c1 in
-	         evar_conv_x ts (push_rel (n,None,c) env) i pbty c'1 c'2)]
+                 let na = Nameops.name_max n1 n2 in
+	         evar_conv_x ts (push_rel (na,None,c) env) i pbty c'1 c'2)]
 
 	| Rel x1, Rel x2 ->
 	    if Int.equal x1 x2 then
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index bfd19c6c7..ac1692f45 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -157,6 +157,7 @@ let restrict_evar_key evd evk filter candidates =
     end
 
 (* Restrict an applied evar and returns its restriction in the same context *)
+(* (the filter is assumed to be at least stronger than the original one) *)
 let restrict_applied_evar evd (evk,argsv) filter candidates =
   let evd,newevk = restrict_evar_key evd evk filter candidates in
   let newargsv = match filter with
@@ -693,7 +694,8 @@ let rec find_projectable_vars with_evars aliases sigma y subst =
     (* Then test if [idc] is (indirectly) bound in [subst] to some evar *)
     (* projectable on [y] *)
       if with_evars then
-        let idcl' = List.filter (fun (c,_,id) -> isEvar c) idcl in
+        let f (c,_,id) = isEvar c && is_undefined sigma (fst (destEvar c)) in
+        let idcl' = List.filter f idcl in
         match idcl' with
         | [c,_,id] ->
           begin
@@ -885,6 +887,9 @@ let filter_candidates evd evk filter candidates_update =
       else
         UpdateWith l'
 
+(* Given a filter refinement for the evar [evk], restrict it so that
+   dependencies are preserved *)
+
 let closure_of_filter evd evk = function
   | None -> None
   | Some filter ->
@@ -892,8 +897,11 @@ let closure_of_filter evd evk = function
   let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in
   let test b (id,c,_) = b || Idset.mem id vars || match c with None -> false | Some c -> not (isRel c || isVar c) in
   let newfilter = Filter.map_along test filter (evar_context evi) in
+  (* Now ensure that restriction is at least what is was originally *)
+  let newfilter = Option.cata (Filter.map_along (&&) newfilter) newfilter (Filter.repr (evar_filter evi)) in
   if Filter.equal newfilter (evar_filter evi) then None else Some newfilter
 
+(* The filter is assumed to be at least stronger than the original one *)
 let restrict_hyps evd evk filter candidates =
     (* What to do with dependencies?
        Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y.
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 90aa8000a..cb091f2d6 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -322,7 +322,8 @@ let instantiate_params t args sign =
 let get_constructor ((ind,u as indu),mib,mip,params) j =
   assert (j <= Array.length mip.mind_consnames);
   let typi = mis_nf_constructor_type (indu,mib,mip) j in
-  let typi = instantiate_params typi params mib.mind_params_ctxt in
+  let ctx = Vars.subst_instance_context u mib.mind_params_ctxt in
+  let typi = instantiate_params typi params ctx in
   let (args,ccl) = decompose_prod_assum typi in
   let (_,allargs) = decompose_app ccl in
   let vargs = List.skipn (List.length params) allargs in
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index b4b6b8aab..2432b8d29 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -150,14 +150,12 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        begin match engagement env with
-        | Some ImpredicativeSet ->
+        if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        | _ ->
+        else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (sup u1 type0_univ)
-        end
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
     (* Product rule (Prop,Type_i,Type_i) *)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 6dc0d1f3c..7fde7b7ac 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -190,7 +190,7 @@ let cs_pattern_of_constr t =
 (* Intended to always succeed *)
 let compute_canonical_projections (con,ind) =
   let env = Global.env () in
-  let ctx = Environ.constant_context env con in
+  let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in
   let u = Univ.UContext.instance ctx in
   let v = (mkConstU (con,u)) in
   let ctx = Univ.ContextSet.of_context ctx in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 743bc3b19..fb5526552 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -126,9 +126,11 @@ let retype ?(polyprop=true) sigma =
     | App(f,args) ->
         strip_outer_cast
           (subst_type env sigma (type_of env f) (Array.to_list args))
-    | Proj (p,c) -> 
+    | Proj (p,c) ->
        let ty = type_of env c in
-       Inductiveops.type_of_projection_knowing_arg env sigma p c ty
+       (try
+	   Inductiveops.type_of_projection_knowing_arg env sigma p c ty
+	 with Invalid_argument _ -> retype_error BadRecursiveType)
     | Cast (c,_, t) -> t
     | Sort _ | Prod _ -> mkSort (sort_of env cstr)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b5fe5d0b6..24e06007e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -676,7 +676,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	| Evar (evk,_ as ev), Evar (evk',_)
             when not (Evar.Set.mem evk flags.frozen_evars)
               && Evar.equal evk evk' ->
-	    sigma,metasubst,((curenv,ev,cN)::evarsubst)
+            let sigma',b = constr_cmp cv_pb sigma flags cM cN in
+            if b then
+	      sigma',metasubst,evarsubst
+            else
+	      sigma,metasubst,((curenv,ev,cN)::evarsubst)
 	| Evar (evk,_ as ev), _
             when not (Evar.Set.mem evk flags.frozen_evars) 
 	      && not (occur_evar evk cN) ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e50435cda..b8c5fd4cf 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -205,16 +205,20 @@ let print_polymorphism ref =
        else "not universe polymorphic") ]
   else []
 
-let print_primitive_record mipv = function
+let print_primitive_record recflag mipv = function
   | Some (Some (_, ps,_)) ->
-    [pr_id mipv.(0).mind_typename ++ str" is primitive and has eta conversion."]
+    let eta = match recflag with
+    | Decl_kinds.CoFinite -> mt ()
+    | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion"
+    in
+    [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
   | _ -> []
     
 let print_primitive ref =
   match ref with 
   | IndRef ind -> 
     let mib,_ = Global.lookup_inductive ind in
-      print_primitive_record mib.mind_packets mib.mind_record
+      print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record
   | _ -> []
 
 let print_name_infos ref =
@@ -447,7 +451,7 @@ let gallina_print_inductive sp =
   let mipv = mib.mind_packets in
   pr_mutual_inductive_body env sp mib ++
   with_line_skip
-    (print_primitive_record mipv mib.mind_record @
+    (print_primitive_record mib.mind_finite mipv mib.mind_record @
      print_inductive_renames sp mipv @
      print_inductive_implicit_args sp mipv @
      print_inductive_argument_scopes sp mipv)
diff --git a/stm/stm.ml b/stm/stm.ml
index 373fd0ba3..8af1aaafd 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2117,7 +2117,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
              iraise (State.exn_on report_id e)); `Ok
       | VtQuery (false,(report_id,route)), VtNow ->
           (try vernac_interp report_id ~route x
-           with e when Errors.noncritical e ->
+           with e ->
              let e = Errors.push e in
              iraise (State.exn_on report_id e)); `Ok
       | VtQuery (true,(report_id,_)), w ->
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 476d850ac..d2466250a 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -28,7 +28,7 @@
 # Default value when called from a freshly compiled Coq, but can be
 # easily overridden
 BIN := ../bin/
-LIB := ..
+LIB := $(shell cd ..; pwd)
 
 coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite
 bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
diff --git a/test-suite/bugs/opened/3819.v b/test-suite/bugs/closed/3819.v
index 7105a6587..355d23a58 100644
--- a/test-suite/bugs/opened/3819.v
+++ b/test-suite/bugs/closed/3819.v
@@ -1,5 +1,3 @@
-Set Universe Polymorphism.
-
 Record Op := { t : Type ; op : t -> t }.
 
 Canonical Structure OpType : Op := Build_Op Type (fun X => X).
@@ -7,5 +5,5 @@ Canonical Structure OpType : Op := Build_Op Type (fun X => X).
 Lemma test1 (X:Type) : eq (op OpType X)  X.
 Proof eq_refl.
 
-Lemma test2 (A:Type) : eq (op _ A)  A.
-Fail Proof eq_refl.
+Definition test2 (A:Type) : eq (op _ A)  A.
+Proof eq_refl.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4205.v b/test-suite/bugs/closed/4205.v
new file mode 100644
index 000000000..c40dfcc1f
--- /dev/null
+++ b/test-suite/bugs/closed/4205.v
@@ -0,0 +1,8 @@
+(* Testing a regression from 8.5beta1 to 8.5beta2 in evar-evar tactic unification problems *)
+
+
+Inductive test : nat -> nat -> nat -> nat -> Prop :=
+  | test1 : forall m n, test m n m n.
+
+Goal test 1 2 3 4.
+erewrite f_equal2 with (f := fun k l => test _ _ k l).
diff --git a/test-suite/bugs/closed/4240.v b/test-suite/bugs/closed/4240.v
new file mode 100644
index 000000000..083c59fe6
--- /dev/null
+++ b/test-suite/bugs/closed/4240.v
@@ -0,0 +1,12 @@
+(* Check that closure of filter did not restrict the former evar filter *)
+
+Lemma foo (new : nat) : False.
+evar (H1: nat).
+set (H3 := 0).
+assert (H3' := id H3).
+evar (H5: nat).
+clear H3.
+assert (H5 = new).
+unfold H5.
+unfold H1.
+exact (eq_refl new).
diff --git a/test-suite/bugs/closed/4276.v b/test-suite/bugs/closed/4276.v
new file mode 100644
index 000000000..ba82e6c37
--- /dev/null
+++ b/test-suite/bugs/closed/4276.v
@@ -0,0 +1,11 @@
+Set Primitive Projections.
+
+Record box (T U : Type) (x := T) := wrap { unwrap : T }.
+Definition mybox : box True False := wrap _ _ I.
+Definition unwrap' := @unwrap.
+
+Definition bad' : True := mybox.(unwrap _ _). 
+
+Fail Definition bad : False := unwrap _ _ mybox.
+
+(* Closed under the global context *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4283.v b/test-suite/bugs/closed/4283.v
new file mode 100644
index 000000000..e06998b71
--- /dev/null
+++ b/test-suite/bugs/closed/4283.v
@@ -0,0 +1,8 @@
+Require Import Hurkens.
+
+Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Definition unwrap' := fun (X : Type) (b : box X) => let (unwrap) := b in unwrap.
+
+Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ Type)) eq_refl.
+
diff --git a/test-suite/coqchk/primproj.v b/test-suite/coqchk/primproj.v
new file mode 100644
index 000000000..04d0a2b6f
--- /dev/null
+++ b/test-suite/coqchk/primproj.v
@@ -0,0 +1,2 @@
+Set Primitive Projections.
+Record foo (T : Type) := { bar : T}.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index dc22b03f2..957612ef1 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -308,3 +308,15 @@ Definition RLRL' : forall x : R, RL x = RL (RL x).
 Qed.
 
 End eta.
+
+Module Hurkens'.
+  Require Import Hurkens.
+
+Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
+
+Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
+Type)) eq_refl.
+
+End Hurkens'.
\ No newline at end of file
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index a2cc8384c..7f2fe741e 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -249,7 +249,7 @@ let files = ref []
 let parse_cl () =
   Arg.parse
       [ "-o", Arg.String (fun s -> output_specified := true; output := s),
-	"output-file    Specifiy the resulting LaTeX file";
+	"output-file    Specify the resulting LaTeX file";
 	"-n", Arg.Int (fun n -> linelen := n),
 	"line-width     Set the line width";
 	"-image", Arg.String (fun s -> image := s),
@@ -265,7 +265,7 @@ let parse_cl () =
 	"-small", Arg.Set small,
 	"           Coq parts are written in small font";
 	"-boot", Arg.Set boot,
-	"           Launch coqtop with the -boot option"
+	"            Launch coqtop with the -boot option"
       ]
       (fun s -> files := s :: !files)
       "coq-tex [options] file ..."
@@ -290,7 +290,7 @@ let main () =
     let _ = Sys.command (!image ^ " -batch") in
     exit 1
   end else begin
-    Printf.printf "Your version of coqtop seems OK\n";
+    (*Printf.printf "Your version of coqtop seems OK\n";*)
     flush stdout
   end;
   List.iter one_file (List.rev !files)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 77339aef4..04238da2b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -360,8 +360,7 @@ let make_conclusion_flexible evdref ty poly =
   else () 
 	
 let is_impredicative env u = 
-  u = Prop Null || 
-  (engagement env = Some Declarations.ImpredicativeSet && u = Prop Pos)
+  u = Prop Null || (is_impredicative_set env && u = Prop Pos)
 
 let interp_ind_arity env evdref ind =
   let c = intern_gen IsType env ind.ind_arity in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c92c8fff7..15065afda 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -112,14 +112,12 @@ let print_memory_stat () =
 
 let _ = at_exit print_memory_stat
 
-let engagement = ref None
-let set_engagement c = engagement := Some c
+let impredicative_set = ref Declarations.PredicativeSet
+let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet
+let type_in_type = ref Declarations.StratifiedType
+let set_type_in_type () = type_in_type := Declarations.TypeInType
 let engage () =
-  match !engagement with Some c -> Global.set_engagement c | None -> ()
-
-let type_in_type = ref false
-let set_type_in_type () = type_in_type := true
-let set_hierarchy () = if !type_in_type then Global.set_type_in_type ()
+  Global.set_engagement (!impredicative_set,!type_in_type)
 
 let set_batch_mode () = batch_mode := true
 
@@ -521,7 +519,7 @@ let parse_args arglist =
     |"-filteropts" -> filter_opts := true
     |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
     |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true
-    |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
+    |"-impredicative-set" -> set_impredicative_set ()
     |"-indices-matter" -> Indtypes.enforce_indices_matter ()
     |"-just-parsing" -> Vernac.just_parsing := true
     |"-m"|"--memory" -> memory_stat := true
@@ -605,7 +603,6 @@ let init arglist =
       Mltop.init_known_plugins ();
       set_vm_opt ();
       engage ();
-      set_hierarchy ();
       (* Be careful to set these variables after the inputstate *)
       Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
       Syntax_def.set_compat_notations (not !no_compat_ntn);
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 737b7fb59..15ad18d9c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -135,7 +135,7 @@ let typecheck_params_and_fields def id t ps nots fs =
     let ctx, aritysort = Reduction.dest_arity env0 arity in
       assert(List.is_empty ctx); (* Ensured by above analysis *)
       if Sorts.is_prop aritysort || 
-	(Sorts.is_set aritysort && engagement env0 = Some ImpredicativeSet) then
+	(Sorts.is_set aritysort && is_impredicative_set env0) then
 	evars
       else Evd.set_leq_sort env_ar evars (Type univ) aritysort
   in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index bc8aa2fff..966b95201 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -215,7 +215,7 @@ let display_cmd_header loc com =
 	 str " [" ++ str cmd ++ str "] ");
   Pp.flush_all ()
 
-let rec vernac_com checknav (loc,com) =
+let rec vernac_com verbose checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
@@ -241,7 +241,7 @@ let rec vernac_com checknav (loc,com) =
 
     | v when !just_parsing -> ()
 
-    | v -> Stm.interp (Flags.is_verbose()) (loc,v)
+    | v -> Stm.interp verbose (loc,v)
   in
     try
       checknav loc com;
@@ -268,7 +268,7 @@ and read_vernac_file verbosely s =
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc_ast = parse_sentence input in
-      vernac_com checknav loc_ast;
+      vernac_com verbosely checknav loc_ast;
       pp_flush ()
     done
   with any ->   (* whatever the exception *)
@@ -293,7 +293,7 @@ let checknav loc ast =
   if is_deep_navigation_vernac ast then
     user_error loc "Navigation commands forbidden in nested commands"
 
-let eval_expr loc_ast = vernac_com checknav loc_ast
+let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
 
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =