Imported Upstream version 8.5~beta3+dfsg

33 files changed, 1189 insertions, 717 deletions

diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
new file mode 100644
index 00000000..a6bd968e
--- /dev/null
+++ b/toplevel/assumptions.ml
@@ -0,0 +1,230 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* The following definitions are used by the function
+   [assumptions] which gives as an output the set of all
+   axioms and sections variables on which a given term depends
+   in a context (expectingly the Global context) *)
+
+(* Initial author: Arnaud Spiwack
+   Module-traversing code: Pierre Letouzey *)
+
+open Pp
+open Errors
+open Util
+open Names
+open Term
+open Declarations
+open Mod_subst
+open Globnames
+open Printer
+
+(** For a constant c in a module sealed by an interface (M:T and
+    not M<:T), [Global.lookup_constant] may return a [constant_body]
+    without body. We fix this by looking in the implementation
+    of the module *)
+
+let modcache = ref (MPmap.empty : structure_body MPmap.t)
+
+let rec search_mod_label lab = function
+  | [] -> raise Not_found
+  | (l, SFBmodule mb) :: _ when Label.equal l lab -> mb
+  | _ :: fields -> search_mod_label lab fields
+
+let rec search_cst_label lab = function
+  | [] -> raise Not_found
+  | (l, SFBconst cb) :: _ when Label.equal l lab -> cb
+  | _ :: fields -> search_cst_label lab fields
+
+(* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But:
+    a) I don't see currently what should be used instead
+    b) this shouldn't be critical for Print Assumption. At worse some
+       constants will have a canonical name which is non-canonical,
+       leading to failures in [Global.lookup_constant], but our own
+       [lookup_constant] should work.
+*)
+
+let rec fields_of_functor f subs mp0 args = function
+  |NoFunctor a -> f subs mp0 args a
+  |MoreFunctor (mbid,_,e) ->
+    match args with
+    | [] -> assert false (* we should only encounter applied functors *)
+    | mpa :: args ->
+      let subs = join (map_mbid mbid mpa empty_delta_resolver (*TODO*)) subs in
+      fields_of_functor f subs mp0 args e
+
+let rec lookup_module_in_impl mp =
+  try Global.lookup_module mp
+  with Not_found ->
+    (* The module we search might not be exported by its englobing module(s).
+       We access the upper layer, and then do a manual search *)
+    match mp with
+    | MPfile _ -> raise Not_found (* can happen if mp is an open module *)
+    | MPbound _ -> assert false
+    | MPdot (mp',lab') ->
+       let fields = memoize_fields_of_mp mp' in
+       search_mod_label lab' fields
+
+and memoize_fields_of_mp mp =
+  try MPmap.find mp !modcache
+  with Not_found ->
+    let l = fields_of_mp mp in
+    modcache := MPmap.add mp l !modcache;
+    l
+
+and fields_of_mp mp =
+  let mb = lookup_module_in_impl mp in
+  let fields,inner_mp,subs = fields_of_mb empty_subst mb [] in
+  let subs =
+    if mp_eq inner_mp mp then subs
+    else add_mp inner_mp mp mb.mod_delta subs
+  in
+  Modops.subst_structure subs fields
+
+and fields_of_mb subs mb args = match mb.mod_expr with
+  |Algebraic expr -> fields_of_expression subs mb.mod_mp args expr
+  |Struct sign -> fields_of_signature subs mb.mod_mp args sign
+  |Abstract|FullStruct -> fields_of_signature subs mb.mod_mp args mb.mod_type
+
+(** The Abstract case above corresponds to [Declare Module] *)
+
+and fields_of_signature x =
+  fields_of_functor
+    (fun subs mp0 args struc ->
+      assert (List.is_empty args);
+      (struc, mp0, subs)) x
+
+and fields_of_expr subs mp0 args = function
+  |MEident mp ->
+    let mb = lookup_module_in_impl (subst_mp subs mp) in
+    fields_of_mb subs mb args
+  |MEapply (me1,mp2) -> fields_of_expr subs mp0 (mp2::args) me1
+  |MEwith _ -> assert false (* no 'with' in [mod_expr] *)
+
+and fields_of_expression x = fields_of_functor fields_of_expr x
+
+let lookup_constant_in_impl cst fallback =
+  try
+    let mp,dp,lab = repr_kn (canonical_con cst) in
+    let fields = memoize_fields_of_mp mp in
+    (* A module found this way is necessarily closed, in particular
+       our constant cannot be in an opened section : *)
+    search_cst_label lab fields
+  with Not_found ->
+    (* Either:
+       - The module part of the constant isn't registered yet :
+         we're still in it, so the [constant_body] found earlier
+         (if any) was a true axiom.
+       - The label has not been found in the structure. This is an error *)
+    match fallback with
+      | Some cb -> cb
+      | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst)
+
+let lookup_constant cst =
+  try
+    let cb = Global.lookup_constant cst in
+    if Declareops.constant_has_body cb then cb
+    else lookup_constant_in_impl cst (Some cb)
+  with Not_found -> lookup_constant_in_impl cst None
+
+(** Graph traversal of an object, collecting on the way the dependencies of
+    traversed objects *)
+
+let label_of = function
+  | ConstRef kn -> pi3 (repr_con kn)
+  | IndRef (kn,_)
+  | ConstructRef ((kn,_),_) -> pi3 (repr_mind kn)
+  | VarRef id -> Label.of_id id
+
+let push (r : Context.rel_declaration) (ctx : Context.rel_context) = r :: ctx
+
+let rec traverse current ctx accu t = match kind_of_term t with
+| Var id ->
+  let body () = match Global.lookup_named id with (_, body, _) -> body in
+  traverse_object accu body (VarRef id)
+| Const (kn, _) ->
+  let body () = Global.body_of_constant_body (lookup_constant kn) in
+  traverse_object accu body (ConstRef kn)
+| Ind (ind, _) ->
+  traverse_object accu (fun () -> None) (IndRef ind)
+| Construct (cst, _) ->
+  traverse_object accu (fun () -> None) (ConstructRef cst)
+| Meta _ | Evar _ -> assert false
+| Case (_,oty,c,[||]) ->
+    (* non dependent match on an inductive with no constructors *) 
+    begin match Constr.(kind oty, kind c) with
+    | Lambda(Anonymous,_,oty), Const (kn, _)
+      when Vars.noccurn 1 oty &&
+      not (Declareops.constant_has_body (lookup_constant kn)) ->
+        let body () = Global.body_of_constant_body (lookup_constant kn) in
+        traverse_object
+          ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
+    | _ ->
+        Termops.fold_constr_with_full_binders push (traverse current) ctx accu t
+    end
+| _ -> Termops.fold_constr_with_full_binders push (traverse current) ctx accu t
+
+and traverse_object ?inhabits (curr, data, ax2ty) body obj =
+  let data, ax2ty =
+    let already_in = Refmap_env.mem obj data in
+    match body () with
+    | None ->
+        let data =
+          if not already_in then Refmap_env.add obj Refset_env.empty data else data in
+        let ax2ty =
+          if Option.is_empty inhabits then ax2ty else
+          let ty = Option.get inhabits in
+          try let l = Refmap_env.find obj ax2ty in Refmap_env.add obj (ty::l) ax2ty 
+          with Not_found -> Refmap_env.add obj [ty] ax2ty in
+        data, ax2ty
+    | Some body ->
+      if already_in then data, ax2ty else
+      let contents,data,ax2ty =
+        traverse (label_of obj) [] (Refset_env.empty,data,ax2ty) body in
+      Refmap_env.add obj contents data, ax2ty
+  in
+  (Refset_env.add obj curr, data, ax2ty)
+
+let traverse current t =
+  let () = modcache := MPmap.empty in
+  traverse current [] (Refset_env.empty, Refmap_env.empty, Refmap_env.empty) t
+
+(** Hopefully bullet-proof function to recover the type of a constant. It just
+    ignores all the universe stuff. There are many issues that can arise when
+    considering terms out of any valid environment, so use with caution. *)
+let type_of_constant cb = match cb.Declarations.const_type with
+| Declarations.RegularArity ty -> ty
+| Declarations.TemplateArity (ctx, arity) ->
+  Term.mkArity (ctx, Sorts.sort_of_univ arity.Declarations.template_level)
+
+let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
+  let (idts, knst) = st in
+  (** Only keep the transitive dependencies *)
+  let (_, graph, ax2ty) = traverse (label_of gr) t in
+  let fold obj _ accu = match obj with
+  | VarRef id ->
+    let (_, body, t) = Global.lookup_named id in
+    if Option.is_empty body then ContextObjectMap.add (Variable id) t accu
+    else accu
+  | ConstRef kn ->
+    let cb = lookup_constant kn in
+    if not (Declareops.constant_has_body cb) then
+      let t = type_of_constant cb in
+      let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+      ContextObjectMap.add (Axiom (kn,l)) t accu
+    else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
+      let t = type_of_constant cb in
+      ContextObjectMap.add (Opaque kn) t accu
+    else if add_transparent then
+      let t = type_of_constant cb in
+      ContextObjectMap.add (Transparent kn) t accu
+    else
+      accu
+  | IndRef _ | ConstructRef _ -> accu
+  in
+  Refmap_env.fold fold graph ContextObjectMap.empty
diff --git a/toplevel/assumptions.mli b/toplevel/assumptions.mli
new file mode 100644
index 00000000..9c9f81bd
--- /dev/null
+++ b/toplevel/assumptions.mli
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Names
+open Term
+open Globnames
+open Printer
+
+(** Collects all the objects on which a term directly relies, bypassing kernel
+    opacity, together with the recursive dependence DAG of objects.
+
+    WARNING: some terms may not make sense in the environment, because they are
+    sealed inside opaque modules. Do not try to do anything fancy with those
+    terms apart from printing them, otherwise demons may fly out of your nose.
+*)
+val traverse :
+  Label.t -> constr ->
+    (Refset_env.t * Refset_env.t Refmap_env.t *
+     (label * Context.rel_context * types) list Refmap_env.t)
+
+(** Collects all the assumptions (optionally including opaque definitions)
+   on which a term relies (together with their type). The above warning of
+   {!traverse} also applies. *)
+val assumptions :
+  ?add_opaque:bool -> ?add_transparent:bool -> transparent_state ->
+     global_reference -> constr -> Term.types ContextObjectMap.t
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 26b54a73..7a89b9f5 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -19,6 +19,7 @@ open Termops
 open Declarations
 open Names
 open Globnames
+open Nameops
 open Inductiveops
 open Tactics
 open Ind_tables
@@ -54,6 +55,7 @@ exception InductiveWithProduct
 exception InductiveWithSort
 exception ParameterWithoutEquality of constant
 exception NonSingletonProp of inductive
+exception DecidabilityMutualNotSupported
 
 let dl = Loc.ghost
 
@@ -109,7 +111,7 @@ let check_bool_is_defined () =
 
 let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
-let build_beq_scheme kn =
+let build_beq_scheme mode kn =
   check_bool_is_defined ();
   (* fetching global env *)
   let env = Global.env() in
@@ -177,23 +179,22 @@ let build_beq_scheme kn =
       let rec aux c =
 	let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in
 	match kind_of_term c with
-        | Rel x -> mkRel (x-nlist+ndx), Declareops.no_seff
-        | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Declareops.no_seff
+        | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
+        | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Safe_typing.empty_private_constants
         | Cast (x,_,_) -> aux (applist (x,a))
         | App _ -> assert false
         | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> 
-            if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Declareops.no_seff
+            if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
             else begin
               try
                 let eq, eff =
-                  let c, eff = find_scheme (!beq_scheme_kind_aux()) (kn',i) in
+                  let c, eff = find_scheme ~mode (!beq_scheme_kind_aux()) (kn',i) in
                   mkConst c, eff in
                 let eqa, eff =
                   let eqa, effs = List.split (List.map aux a) in
                   Array.of_list eqa,
-                  Declareops.union_side_effects
-                    (Declareops.flatten_side_effects (List.rev effs))
-                    eff in
+                  List.fold_left Safe_typing.concat_private eff (List.rev effs)
+                  in
                 let args =
                   Array.append 
                     (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in
@@ -236,7 +237,7 @@ let build_beq_scheme kn =
     let constrsi = constrs (3+nparrec) in
     let n = Array.length constrsi in
     let ar = Array.make n (Lazy.force ff) in
-    let eff = ref Declareops.no_seff in
+    let eff = ref Safe_typing.empty_private_constants in
 	for i=0 to n-1 do
 	  let nb_cstr_args = List.length constrsi.(i).cs_args in
 	  let ar2 = Array.make n (Lazy.force ff) in
@@ -254,7 +255,7 @@ let build_beq_scheme kn =
                                           (nb_cstr_args+ndx+1)
                                           cc
                           in
-                          eff := Declareops.union_side_effects eff' !eff;
+                          eff := Safe_typing.concat_private eff' !eff;
                           Array.set eqs ndx
                               (mkApp (eqA,
                                 [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|]
@@ -286,7 +287,7 @@ let build_beq_scheme kn =
     let names = Array.make nb_ind Anonymous and
         types = Array.make nb_ind mkSet and
         cores = Array.make nb_ind mkSet in
-    let eff = ref Declareops.no_seff in
+    let eff = ref Safe_typing.empty_private_constants in
     let u = Univ.Instance.empty in
     for i=0 to (nb_ind-1) do
         names.(i) <- Name (Id.of_string (rec_name i));
@@ -294,7 +295,7 @@ let build_beq_scheme kn =
                      (mkArrow (mkFullInd ((kn,i),u) 1) (Lazy.force bb));
         let c, eff' = make_one_eq i in
         cores.(i) <- c;
-        eff := Declareops.union_side_effects eff' !eff
+        eff := Safe_typing.concat_private eff' !eff
     done;
       (Array.init nb_ind (fun i ->
       let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
@@ -302,7 +303,7 @@ let build_beq_scheme kn =
 	  raise (NonSingletonProp (kn,i));
         let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
         create_input fix),
-       Evd.empty_evar_universe_context (* FIXME *)),
+       Evd.make_evar_universe_context (Global.env ()) None),
       !eff
 
 let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme
@@ -328,7 +329,7 @@ let destruct_ind c =
 so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
 *)
 (* used in the leib -> bool side*)
-let do_replace_lb lb_scheme_key aavoid narg p q =
+let do_replace_lb mode lb_scheme_key aavoid narg p q =
   let avoid = Array.of_list aavoid in
   let do_arg v offset =
   try
@@ -338,7 +339,8 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
     let rec find i =
       if Id.equal avoid.(n-i) s then avoid.(n-i-x)
       else (if i<n then find (i+1)
-            else error ("Var "^(Id.to_string s)^" seems unknown.")
+            else errorlabstrm "AutoIndDecl.do_replace_lb"
+                   (str "Var " ++ pr_id s ++ str " seems unknown.")
       )
     in mkVar (find 1)
   with e when Errors.noncritical e ->
@@ -353,11 +355,11 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
       )
   in
   Proofview.Goal.nf_enter begin fun gl ->
-    let type_of_pq = Tacmach.New.of_old (fun gl -> pf_type_of gl p) gl in
+    let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in
     let u,v = destruct_ind type_of_pq
     in let lb_type_of_p =
         try
-          let c, eff = find_scheme lb_scheme_key (out_punivs u) (*FIXME*) in
+          let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in
           Proofview.tclUNIT (mkConst c, eff)
         with Not_found ->
           (* spiwack: the format of this error message should probably
@@ -369,7 +371,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
 	     Printer.pr_constr type_of_pq ++
 	     str " first.")
           in
-          Proofview.tclZERO (Errors.UserError("",err_msg))
+          Tacticals.New.tclZEROMSG err_msg
        in
        lb_type_of_p >>= fun (lb_type_of_p,eff) ->
        let lb_args = Array.append (Array.append
@@ -385,7 +387,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
   end
 
 (* used in the bool -> leib side *)
-let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
+let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
   let avoid = Array.of_list aavoid in
   let do_arg v offset =
   try
@@ -395,7 +397,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
     let rec find i =
       if Id.equal avoid.(n-i) s then avoid.(n-i-x)
       else (if i<n then find (i+1)
-            else error ("Var "^(Id.to_string s)^" seems unknown.")
+            else errorlabstrm "AutoIndDecl.do_replace_bl"
+                   (str "Var " ++ pr_id s ++ str " seems unknown.")
       )
     in mkVar (find 1)
   with e when Errors.noncritical e ->
@@ -414,7 +417,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
     match (l1,l2) with
     | (t1::q1,t2::q2) ->
         Proofview.Goal.enter begin fun gl ->
-        let tt1 = Tacmach.New.pf_type_of gl t1 in
+        let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
         if eq_constr t1 t2 then aux q1 q2
         else (
           let u,v = try  destruct_ind tt1
@@ -456,28 +459,28 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
         )
         end
     | ([],[]) -> Proofview.tclUNIT ()
-    | _ -> Proofview.tclZERO (UserError ("" , str"Both side of the equality must have the same arity."))
+    | _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.")
   in
   begin try Proofview.tclUNIT (destApp lft)
-    with DestKO ->  Proofview.tclZERO (UserError ("" , str"replace failed."))
+    with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.")
   end >>= fun (ind1,ca1) ->
   begin try Proofview.tclUNIT (destApp rgt)
-    with DestKO -> Proofview.tclZERO (UserError ("" , str"replace failed."))
+    with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.")
   end >>= fun (ind2,ca2) ->
   begin try Proofview.tclUNIT (out_punivs (destInd ind1))
     with DestKO ->
       begin try Proofview.tclUNIT (fst (fst (destConstruct ind1)))
-        with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
+        with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
       end
   end >>= fun (sp1,i1) ->
   begin try Proofview.tclUNIT (out_punivs (destInd ind2))
     with DestKO ->
       begin try Proofview.tclUNIT (fst (fst (destConstruct ind2)))
-        with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
+        with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
       end
   end >>= fun (sp2,i2) ->
   if not (eq_mind sp1 sp2) || not (Int.equal i1 i2)
-  then Proofview.tclZERO (UserError ("" , str"Eq should be on the same type"))
+  then Tacticals.New.tclZEROMSG (str "Eq should be on the same type")
   else aux (Array.to_list ca1) (Array.to_list ca2)
 
 (*
@@ -502,8 +505,8 @@ let eqI ind l =
                            (List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
   and e, eff = 
     try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff 
-    with Not_found -> error
-        ("The boolean equality on "^(string_of_mind (fst ind))^" is needed.");
+    with Not_found -> errorlabstrm "AutoIndDecl.eqI"
+      (str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed.");
   in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)), eff
 
 (**********************************************************************)
@@ -547,7 +550,7 @@ let compute_bl_goal ind lnamesparrec nparrec =
               (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
         ))), eff
 
-let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec =
+let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
   let avoid = ref [] in
       let first_intros =
@@ -604,16 +607,16 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                               if eq_gr (IndRef indeq) Coqlib.glob_eq
                               then
                                 Tacticals.New.tclTHEN
-                                  (do_replace_bl bl_scheme_key ind
+                                  (do_replace_bl mode bl_scheme_key ind
 				     (!avoid)
                                      nparrec (ca.(2))
                                      (ca.(1)))
                                   Auto.default_auto
                               else
-                                Proofview.tclZERO (UserError ("",str"Failure while solving Boolean->Leibniz."))
-                          | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz."))
+                                Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
+                          | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.")
                         )
-                        | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz."))
+                        | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
                       end
 
                     ]
@@ -621,7 +624,12 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 
 let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
-let make_bl_scheme mind =
+let side_effect_of_mode = function
+  | Declare.UserAutomaticRequest -> false
+  | Declare.InternalTacticRequest -> true
+  | Declare.UserIndividualRequest -> false
+
+let make_bl_scheme mode mind =
   let mib = Global.lookup_mind mind in
   if not (Int.equal (Array.length mib.mind_packets) 1) then
     errorlabstrm ""
@@ -632,9 +640,10 @@ let make_bl_scheme mind =
   let lnonparrec,lnamesparrec = (* TODO subst *)
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
-  let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in
-  let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx bl_goal
-    (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
+  let ctx = Evd.make_evar_universe_context (Global.env ()) None in
+  let side_eff = side_effect_of_mode mode in
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal
+    (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
   in
   ([|ans|], ctx), eff
 
@@ -684,7 +693,7 @@ let compute_lb_goal ind lnamesparrec nparrec =
               (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
         ))), eff
 
-let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
+let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
     let avoid = ref [] in
       let first_intros =
@@ -728,22 +737,22 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
                         | App(c,ca) -> (match (kind_of_term ca.(1)) with
                           | App(c',ca') ->
                               let n = Array.length ca' in
-                              do_replace_lb lb_scheme_key
+                              do_replace_lb mode lb_scheme_key
 				(!avoid)
                                 nparrec
                                 ca'.(n-2) ca'.(n-1)
                           | _ ->
-                              Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean."))
+                              Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
                         )
                         | _ ->
-                            Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean."))
+                            Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
                       end
                     ]
       end
 
 let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
 
-let make_lb_scheme mind =
+let make_lb_scheme mode mind =
   let mib = Global.lookup_mind mind in
   if not (Int.equal (Array.length mib.mind_packets) 1) then
     errorlabstrm ""
@@ -754,11 +763,12 @@ let make_lb_scheme mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
-  let ctx = Evd.empty_evar_universe_context in
-  let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx lb_goal
-    (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
+  let ctx = Evd.make_evar_universe_context (Global.env ()) None in
+  let side_eff = side_effect_of_mode mode in
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal
+    (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
   in
-  ([|ans|], ctx (* FIXME *)), eff
+  ([|ans|], ctx), eff
 
 let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme
 
@@ -856,17 +866,15 @@ let compute_dec_tact ind lnamesparrec nparrec =
           let c, eff = find_scheme bl_scheme_kind ind in
           Proofview.tclUNIT (mkConst c,eff) with
     Not_found ->
-      Proofview.tclZERO (UserError ("",str"Error during the decidability part, boolean to leibniz"++
-        str" equality is required."))
+      Tacticals.New.tclZEROMSG (str "Error during the decidability part, boolean to leibniz equality is required.")
   end >>= fun (blI,eff') ->
   begin try
           let c, eff = find_scheme lb_scheme_kind ind in
           Proofview.tclUNIT (mkConst c,eff) with
     Not_found ->
-      Proofview.tclZERO (UserError ("",str"Error during the decidability part, leibniz to boolean"++
-        str" equality is required."))
+      Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.")
   end >>= fun (lbI,eff'') ->
-  let eff = (Declareops.union_side_effects eff'' (Declareops.union_side_effects eff' eff)) in
+  let eff = (Safe_typing.concat_private eff'' (Safe_typing.concat_private eff' eff)) in
   Tacticals.New.tclTHENLIST [
         Proofview.tclEFFECTS eff;
         intros_using fresh_first_intros;
@@ -917,22 +925,23 @@ let compute_dec_tact ind lnamesparrec nparrec =
   ]
   end
 
-let make_eq_decidability mind =
+let make_eq_decidability mode mind =
   let mib = Global.lookup_mind mind in
   if not (Int.equal (Array.length mib.mind_packets) 1) then
-    anomaly (Pp.str "Decidability lemma for mutual inductive types not supported");
+    raise DecidabilityMutualNotSupported;
   let ind = (mind,0) in
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
   let u = Univ.Instance.empty in
-  let ctx = Evd.empty_evar_universe_context (* FIXME *)in
+  let ctx = Evd.make_evar_universe_context (Global.env ()) None in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
-  let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx
+  let side_eff = side_effect_of_mode mode in
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx
     (compute_dec_goal (ind,u) lnamesparrec nparrec)
     (compute_dec_tact ind lnamesparrec nparrec)
   in
-  ([|ans|], ctx), Declareops.no_seff
+  ([|ans|], ctx), Safe_typing.empty_private_constants
 
 let eq_dec_scheme_kind =
   declare_mutual_scheme_object "_eq_dec" make_eq_decidability
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 80787298..20a3d5d7 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -23,6 +23,7 @@ exception InductiveWithProduct
 exception InductiveWithSort
 exception ParameterWithoutEquality of constant
 exception NonSingletonProp of inductive
+exception DecidabilityMutualNotSupported
 
 val beq_scheme_kind : mutual scheme_kind
 val build_beq_scheme : mutual_scheme_object_function
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index b29ba1ef..accba312 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -20,7 +20,7 @@ let print_loc loc =
     let loc = Loc.unloc loc in
     (int (fst loc) ++ str"-" ++ int (snd loc))
 
-let guill s = "\""^s^"\""
+let guill s = str "\"" ++ str s ++ str "\""
 
 (** Invariant : exceptions embedded in EvaluatedError satisfy
     Errors.noncritical *)
@@ -33,10 +33,10 @@ exception EvaluatedError of std_ppcmds * exn option
 
 let explain_exn_default = function
   (* Basic interaction exceptions *)
-  | Stream.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ "."))
-  | Compat.Token.Error txt ->  hov 0 (str ("Syntax error: " ^ txt ^ "."))
+  | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
+  | Compat.Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
   | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err))
-  | Sys_error msg -> hov 0 (str ("System error: " ^ guill msg))
+  | Sys_error msg -> hov 0 (str "System error: " ++ guill msg)
   | Out_of_memory -> hov 0 (str "Out of memory.")
   | Stack_overflow -> hov 0 (str "Stack overflow.")
   | Timeout -> hov 0 (str "Timeout!")
@@ -110,9 +110,16 @@ let rec strip_wrapping_exceptions = function
     strip_wrapping_exceptions e
   | exc -> exc
 
-let process_vernac_interp_error ?(with_header=true) (exc, info) =
+let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) =
   let exc = strip_wrapping_exceptions exc in
   let e = process_vernac_interp_error with_header (exc, info) in
+  let () =
+    if not allow_uncaught && not (Errors.handled (fst e)) then
+      let (e, info) = e in
+      let msg = str "Uncaught exception " ++ str (Printexc.to_string e) in
+      let err = Errors.make_anomaly msg in
+      Util.iraise (err, info)
+  in
   let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in
   let loc = Option.default Loc.ghost (Loc.get_loc info) in
   match ltac_trace with
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 100b3772..729686f3 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -12,7 +12,7 @@ val print_loc : Loc.t -> Pp.std_ppcmds
 
 (** Pre-explain a vernac interpretation error *)
 
-val process_vernac_interp_error : ?with_header:bool -> Util.iexn -> Util.iexn
+val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn
 
 (** General explain function. Should not be used directly now,
     see instead function [Errors.print] and variants *)
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 6a485d52..da662403 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -186,8 +186,9 @@ let error_not_transparent source =
 
 let build_id_coercion idf_opt source poly =
   let env = Global.env () in
-  let vs, ctx = match source with
-    | CL_CONST sp -> Universes.fresh_global_instance env (ConstRef sp)
+  let sigma = Evd.from_env env in
+  let sigma, vs = match source with
+    | CL_CONST sp -> Evd.fresh_global env sigma (ConstRef sp)
     | _ -> error_not_transparent source in
   let c = match constant_opt_value_in env (destConst vs) with
     | Some c -> c
@@ -208,8 +209,8 @@ let build_id_coercion idf_opt source poly =
   (* juste pour verification *)
   let _ =
     if not
-      (Reductionops.is_conv_leq env Evd.empty
-	(Typing.type_of env Evd.empty val_f) typ_f)
+      (Reductionops.is_conv_leq env sigma
+	(Typing.unsafe_type_of env sigma val_f) typ_f)
     then
       errorlabstrm "" (strbrk
 	"Cannot be defined as coercion (maybe a bad number of arguments).")
@@ -218,13 +219,13 @@ let build_id_coercion idf_opt source poly =
     match idf_opt with
       | Some idf -> idf
       | None ->
-	  let cl,u,_ = find_class_type Evd.empty t in
+	  let cl,u,_ = find_class_type sigma t in
 	  Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
                         (ident_key_of_class cl))
   in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
-      (definition_entry ~types:typ_f ~poly ~univs:(Univ.ContextSet.to_context ctx)
+      (definition_entry ~types:typ_f ~poly ~univs:(snd (Evd.universe_context sigma))
 	 ~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
   in
   let decl = (constr_entry, IsDefinition IdentityCoercion) in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 33891ad9..c354c7d3 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -185,9 +185,9 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	    nf t
 	in
 	Evarutil.check_evars env Evd.empty !evars termtype;
-	let ctx = Evd.universe_context !evars in
-	let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
-	  (Entries.ParameterEntry 
+	let pl, ctx = Evd.universe_context !evars in
+	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
+	  (ParameterEntry 
             (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in instance_hook k None global imps ?hook (ConstRef cst); id
       end
@@ -347,7 +347,7 @@ let named_of_rel_context l =
 
 let context poly l =
   let env = Global.env() in
-  let evars = ref Evd.empty in
+  let evars = ref (Evd.from_env env) in
   let _, ((env', fullctx), impls) = interp_context_evars env evars l in
   let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
   let fullctx = Context.map_rel_context subst fullctx in
@@ -358,12 +358,14 @@ let context poly l =
     with e when Errors.noncritical e ->
       error "Anonymous variables not allowed in contexts."
   in
-  let uctx = Evd.universe_context_set !evars in
+  let uctx = ref (Evd.universe_context_set !evars) in
   let fn status (id, b, t) =
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
-      let uctx = Univ.ContextSet.to_context uctx in	
-      let decl = (ParameterEntry (None,poly,(t,uctx),None), IsAssumption Logical) in
-      let cst = Declare.declare_constant ~internal:Declare.KernelSilent id decl in
+      let ctx = Univ.ContextSet.to_context !uctx in
+      (* Declare the universe context once *)
+      let () = uctx := Univ.ContextSet.empty in
+      let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in
+      let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
 	match class_of_constr t with
 	| Some (rels, ((tc,_), args) as _cl) ->
 	    add_instance (Typeclasses.new_instance tc None false (*FIXME*)
@@ -379,8 +381,9 @@ let context poly l =
       let impl = List.exists test impls in
       let decl = (Discharge, poly, Definitional) in
       let nstatus =
-        pi3 (Command.declare_assumption false decl (t, uctx) [] impl
+        pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl
           Vernacexpr.NoInline (Loc.ghost, id))
       in
-      status && nstatus
+      let () = uctx := Univ.ContextSet.empty in
+	status && nstatus
   in List.fold_left fn true (List.rev ctx)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 754ad852..3d338ee0 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -38,16 +38,16 @@ open Indschemes
 open Misctypes
 open Vernacexpr
 
-let do_universe l = Declare.do_universe l  
-let do_constraint l = Declare.do_constraint l
+let do_universe poly l = Declare.do_universe poly l
+let do_constraint poly l = Declare.do_constraint poly l
 
-let rec under_binders env f n c =
-  if Int.equal n 0 then snd (f env Evd.empty c) else
+let rec under_binders env sigma f n c =
+  if Int.equal n 0 then snd (f env sigma c) else
     match kind_of_term c with
       | Lambda (x,t,c) ->
-	  mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c)
+	  mkLambda (x,t,under_binders (push_rel (x,None,t) env) sigma f (n-1) c)
       | LetIn (x,b,t,c) ->
-	  mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) f (n-1) c)
+	  mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) sigma f (n-1) c)
       | _ -> assert false
 
 let rec complete_conclusion a cs = function
@@ -67,22 +67,23 @@ let rec complete_conclusion a cs = function
 
 (* 1| Constant definitions *)
 
-let red_constant_entry n ce = function
+let red_constant_entry n ce sigma = function
   | None -> ce
   | Some red ->
       let proof_out = ce.const_entry_body in
       let env = Global.env () in
       { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out
         (fun ((body,ctx),eff) ->
-          (under_binders env
+          (under_binders env sigma
              (fst (reduction_of_red_expr env red)) n body,ctx),eff) }
 
-let interp_definition bl p red_option c ctypopt =
+let interp_definition pl bl p red_option c ctypopt =
   let env = Global.env() in
-  let evdref = ref (Evd.from_env env) in
+  let ctx = Evd.make_evar_universe_context env pl in
+  let evdref = ref (Evd.from_ctx ctx) in
   let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
   let nb_args = List.length ctx in
-  let imps,ce =
+  let imps,pl,ce =
     match ctypopt with
       None ->
         let subst = evd_comb0 Evd.nf_univ_variables evdref in
@@ -92,10 +93,10 @@ let interp_definition bl p red_option c ctypopt =
         let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
         let body = nf (it_mkLambda_or_LetIn c ctx) in
 	let vars = Universes.universes_of_constr body in
-	let ctx = Universes.restrict_universe_context
-	  (Evd.universe_context_set !evdref) vars in
- 	imps1@(Impargs.lift_implicits nb_args imps2),
-	  definition_entry ~univs:(Univ.ContextSet.to_context ctx) ~poly:p body
+	let evd = Evd.restrict_universe_context !evdref vars in
+	let pl, uctx = Evd.universe_context ?names:pl evd in
+ 	imps1@(Impargs.lift_implicits nb_args imps2), pl,
+	  definition_entry ~univs:uctx ~poly:p body
     | Some ctyp ->
 	let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
 	let subst = evd_comb0 Evd.nf_univ_variables evdref in
@@ -118,15 +119,15 @@ let interp_definition bl p red_option c ctypopt =
 	   strbrk "The term declares more implicits than the type here.");
         let vars = Univ.LSet.union (Universes.universes_of_constr body) 
           (Universes.universes_of_constr typ) in
-        let ctx = Universes.restrict_universe_context
-          (Evd.universe_context_set !evdref) vars in
-	imps1@(Impargs.lift_implicits nb_args impsty),
+        let ctx = Evd.restrict_universe_context !evdref vars in
+	let pl, uctx = Evd.universe_context ?names:pl ctx in
+	imps1@(Impargs.lift_implicits nb_args impsty), pl,
 	  definition_entry ~types:typ ~poly:p 
-	    ~univs:(Univ.ContextSet.to_context ctx) body
+	    ~univs:uctx body
   in
-  red_constant_entry (rel_context_length ctx) ce red_option, !evdref, imps
+  red_constant_entry (rel_context_length ctx) ce !evdref red_option, !evdref, pl, imps
 
-let check_definition (ce, evd, imps) =
+let check_definition (ce, evd, _, imps) =
   check_evars_are_solved (Global.env ()) evd (Evd.empty,evd);
   ce
 
@@ -139,11 +140,12 @@ let get_locality id = function
 | Local -> true
 | Global -> false
 
-let declare_global_definition ident ce local k imps =
+let declare_global_definition ident ce local k pl imps =
   let local = get_locality ident local in
   let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
+  let () = Universes.register_universe_binders gr pl in
   let () = definition_message ident in
   gr
 
@@ -151,7 +153,8 @@ let declare_definition_hook = ref ignore
 let set_declare_definition_hook = (:=) declare_definition_hook
 let get_declare_definition_hook () = !declare_definition_hook
 
-let declare_definition ident (local, p, k) ce imps hook =
+let declare_definition ident (local, p, k) ce pl imps hook =
+  let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let () = !declare_definition_hook ce in
   let r = match local with
   | Discharge when Lib.sections_are_opened () ->
@@ -167,17 +170,18 @@ let declare_definition ident (local, p, k) ce imps hook =
     in
     gr
   | Discharge | Local | Global ->
-    declare_global_definition ident ce local k imps in
-  Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
+    declare_global_definition ident ce local k pl imps in
+  Lemmas.call_hook fix_exn hook local r
 
-let _ = Obligations.declare_definition_ref := declare_definition
+let _ = Obligations.declare_definition_ref :=
+       (fun i k c imps hook -> declare_definition i k c [] imps hook)
 
-let do_definition ident k bl red_option c ctypopt hook =
-  let (ce, evd, imps as def) = interp_definition bl (pi2 k) red_option c ctypopt in
+let do_definition ident k pl bl red_option c ctypopt hook =
+  let (ce, evd, pl, imps as def) = interp_definition pl bl (pi2 k) red_option c ctypopt in
     if Flags.is_program_mode () then
       let env = Global.env () in
       let (c,ctx), sideff = Future.force ce.const_entry_body in
-      assert(Declareops.side_effects_is_empty sideff);
+      assert(Safe_typing.empty_private_constants = sideff);
       assert(Univ.ContextSet.is_empty ctx);
       let typ = match ce.const_entry_type with 
 	| Some t -> t
@@ -191,13 +195,14 @@ let do_definition ident k bl red_option c ctypopt hook =
 	ignore(Obligations.add_definition
           ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(declare_definition ident k ce imps
+      ignore(declare_definition ident k ce pl imps
         (Lemmas.mk_hook
           (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
-let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = match local with
+let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) =
+match local with
 | Discharge when Lib.sections_are_opened () ->
   let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
   let _ = declare_variable ident decl in
@@ -224,6 +229,7 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma
   let kn = declare_constant ident ~local decl in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
+  let () = Universes.register_universe_binders gr pl in
   let () = assumption_message ident in
   let () = Typeclasses.declare_instance None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr local p in
@@ -240,14 +246,17 @@ let interp_assumption evdref env impls bl c =
   let ctx = Evd.universe_context_set evd in
     ((nf ty, ctx), impls)
 
-let declare_assumptions idl is_coe k c imps impl_is_on nl =
-  let refs, status =
-    List.fold_left (fun (refs,status) id ->
-      let ref',u',status' = declare_assumption is_coe k c imps impl_is_on nl id in
-      (ref',u')::refs, status' && status) ([],true) idl in
+let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl =
+  let refs, status, _ =
+    List.fold_left (fun (refs,status,ctx) id ->
+      let ref',u',status' =
+	declare_assumption is_coe k (c,ctx) pl imps impl_is_on nl id in
+      (ref',u')::refs, status' && status, Univ.ContextSet.empty)
+      ([],true,ctx) idl
+  in
   List.rev refs, status
 
-let do_assumptions (_, poly, _ as kind) nl l =
+let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
   let env = Global.env () in
   let evdref = ref (Evd.from_env env) in
   let l = 
@@ -273,13 +282,52 @@ let do_assumptions (_, poly, _ as kind) nl l =
   let l = List.map (on_pi2 (nf_evar evd)) l in
   snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) ->
     let t = replace_vars subst t in
-    let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) imps false nl in
+    let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in
     let subst' = List.map2 
       (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u)))
       idl refs 
     in
       (subst'@subst, status' && status)) ([],true) l)
 
+let do_assumptions_bound_univs coe kind nl id pl c =
+  let env = Global.env () in
+  let ctx = Evd.make_evar_universe_context env pl in
+  let evdref = ref (Evd.from_ctx ctx) in
+  let ty, impls = interp_type_evars_impls env evdref c in
+  let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
+  let ty = nf ty in
+  let vars = Universes.universes_of_constr ty in
+  let evd = Evd.restrict_universe_context !evdref vars in
+  let pl, uctx = Evd.universe_context ?names:pl evd in
+  let uctx = Univ.ContextSet.of_context uctx in
+  let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in
+  st
+
+let do_assumptions kind nl l = match l with
+| [coe, ([id, Some pl], c)] ->
+  let () = match kind with
+  | (Discharge, _, _) when Lib.sections_are_opened () ->
+    let loc = fst id in
+    let msg = Pp.str "Section variables cannot be polymorphic." in
+    user_err_loc (loc, "", msg)
+  | _ -> ()
+  in
+  do_assumptions_bound_univs coe kind nl id (Some pl) c
+| _ ->
+  let map (coe, (idl, c)) =
+    let map (id, univs) = match univs with
+    | None -> id
+    | Some _ ->
+      let loc = fst id in
+      let msg =
+	Pp.str "Assumptions with bound universes can only be defined one at a time." in
+      user_err_loc (loc, "", msg)
+    in
+    (coe, (List.map map idl, c))
+  in
+  let l = List.map map l in
+  do_assumptions_unbound_univs kind nl l
+
 (* 3a| Elimination schemes for mutual inductive definitions *)
 
 (* 3b| Mutual inductive definitions *)
@@ -290,6 +338,7 @@ let push_types env idl tl =
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
+  ind_univs : lident list option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }
@@ -360,8 +409,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
@@ -402,20 +450,33 @@ let extract_level env evd min tys =
       sign_level env evd ((Anonymous, None, concl) :: ctx)) tys 
   in sup_list min sorts
 
+let is_flexible_sort evd u =
+  match Univ.Universe.level u with
+  | Some l -> Evd.is_flexible_level evd l
+  | None -> false
+
 let inductive_levels env evdref poly arities inds =
-  let destarities = List.map (Reduction.dest_arity env) arities in
-  let levels = List.map (fun (ctx,a) -> 
+  let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
+  let levels = List.map (fun (x,(ctx,a)) -> 
     if a = Prop Null then None
     else Some (univ_of_sort a)) destarities
   in
   let cstrs_levels, min_levels, sizes = 
     CList.split3
-      (List.map2 (fun (_,tys,_) (ctx,du) -> 
+      (List.map2 (fun (_,tys,_) (arity,(ctx,du)) -> 
 	let len = List.length tys in
+	let minlev = Sorts.univ_of_sort du in
 	let minlev =
 	  if len > 1 && not (is_impredicative env du) then
-	    Univ.type0_univ
-	  else Univ.type0m_univ
+	    Univ.sup minlev Univ.type0_univ
+	  else minlev
+	in
+	let minlev =
+	  (** Indices contribute. *)
+	  if Indtypes.is_indices_matter () && List.length ctx > 0 then (
+	    let ilev = sign_level env !evdref ctx in
+	      Univ.sup ilev minlev)
+	  else minlev
 	in
 	let clev = extract_level env !evdref minlev tys in
 	  (clev, minlev, len)) inds destarities)
@@ -425,32 +486,25 @@ let inductive_levels env evdref poly arities inds =
   let levels' = Universes.solve_constraints_system (Array.of_list levels)
     (Array.of_list cstrs_levels) (Array.of_list min_levels)
   in
-  let evd =
-    CList.fold_left3 (fun evd cu (ctx,du) len ->
+  let evd, arities =
+    CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
       if is_impredicative env du then
 	(** Any product is allowed here. *)
-	evd
+	evd, arity :: arities
       else (** If in a predicative sort, or asked to infer the type,
 	       we take the max of:
 	       - indices (if in indices-matter mode)
 	       - constructors
 	       - Type(1) if there is more than 1 constructor
 	   *)
-	let evd = 
-	  (** Indices contribute. *)
-	  if Indtypes.is_indices_matter () && List.length ctx > 0 then (
-	    let ilev = sign_level env !evdref ctx in
-	      Evd.set_leq_sort env evd (Type ilev) du)
-	  else evd
-	in
         (** Constructors contribute. *)
 	let evd = 
 	  if Sorts.is_set du then
 	    if not (Evd.check_leq evd cu Univ.type0_univ) then 
 	      raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType)
 	    else evd
-	  else
-	    Evd.set_leq_sort env evd (Type cu) du
+	  else evd
+	    (* Evd.set_leq_sort env evd (Type cu) du *)
 	in
 	let evd = 
 	  if len >= 2 && Univ.is_type0m_univ cu then 
@@ -459,9 +513,20 @@ let inductive_levels env evdref poly arities inds =
 	       land in Prop directly (no informative arguments as well). *)
 	    Evd.set_leq_sort env evd (Prop Pos) du
 	  else evd
-	in evd)
-    !evdref (Array.to_list levels') destarities sizes
-  in evdref := evd; arities
+	in
+	let duu = Sorts.univ_of_sort du in
+	let evd =
+	  if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then
+	    if is_flexible_sort evd duu then
+	      if Evd.check_leq evd Univ.type0_univ duu then
+	      	evd
+	      else Evd.set_eq_sort env evd (Prop Null) du
+	    else evd
+	  else Evd.set_eq_sort env evd (Type cu) du
+	in
+	  (evd, arity :: arities))
+    (!evdref,[]) (Array.to_list levels') destarities sizes
+  in evdref := evd; List.rev arities
 
 let check_named (loc, na) = match na with
 | Name _ -> ()
@@ -479,12 +544,14 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
   let env0 = Global.env() in
-  let evdref = ref Evd.(from_env env0) in
+  let pl = (List.hd indl).ind_univs in
+  let ctx = Evd.make_evar_universe_context env0 pl in
+  let evdref = ref Evd.(from_ctx ctx) in
   let _, ((env_params, ctx_params), userimpls) =
     interp_context_evars env0 evdref paramsl
   in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
-
+      
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   let assums = List.filter(fun (_,b,_) -> Option.is_empty b) ctx_params in
   let params = List.map (fun (na,_,_) -> out_name na) assums in
@@ -526,6 +593,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
   let ctx_params = map_rel_context nf ctx_params in
   let evd = !evdref in
+  let pl, uctx = Evd.universe_context ?names:pl evd in
   List.iter (check_evars env_params Evd.empty evd) arities;
   iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
   List.iter (fun (_,ctyps,_) ->
@@ -553,8 +621,8 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     mind_entry_inds = entries;
     mind_entry_polymorphic = poly;
     mind_entry_private = if prv then Some false else None;
-    mind_entry_universes = Evd.universe_context evd },
-    impls
+    mind_entry_universes = uctx },
+    pl, impls
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
@@ -575,8 +643,8 @@ let extract_params indl =
       params
 
 let extract_inductive indl =
-  List.map (fun ((_,indname),_,ar,lc) -> {
-    ind_name = indname;
+  List.map (fun (((_,indname),pl),_,ar,lc) -> {
+    ind_name = indname; ind_univs = pl;
     ind_arity = Option.cata (fun x -> x) (CSort (Loc.ghost,GType [])) ar;
     ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
   }) indl
@@ -603,14 +671,13 @@ let is_recursive mie =
       List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc
   | _ -> false
 
-let declare_mutual_inductive_with_eliminations mie impls =
+let declare_mutual_inductive_with_eliminations mie pl impls =
   (* spiwack: raises an error if the structure is supposed to be non-recursive,
         but isn't *)
   begin match mie.mind_entry_finite with
   | BiFinite when is_recursive mie ->
       if Option.has_some mie.mind_entry_record then
-        error ("Records declared with the keywords Record or Structure cannot be recursive." ^
-                  "You can, however, define recursive records using the Inductive or CoInductive command.")
+        error "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command."
       else
         error ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")
   | _ -> ()
@@ -619,12 +686,15 @@ let declare_mutual_inductive_with_eliminations mie impls =
   let (_, kn), prim = declare_mind mie in
   let mind = Global.mind_of_delta_kn kn in
   List.iteri (fun i (indimpls, constrimpls) ->
-		   let ind = (mind,i) in
-		     maybe_declare_manual_implicits false (IndRef ind) indimpls;
-		     List.iteri
-		       (fun j impls ->
-			  maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls)
-		       constrimpls)
+	      let ind = (mind,i) in
+	      let gr = IndRef ind in
+	      maybe_declare_manual_implicits false gr indimpls;
+	      Universes.register_universe_binders gr pl;
+	      List.iteri
+		(fun j impls ->
+		 maybe_declare_manual_implicits false
+		    (ConstructRef (ind, succ j)) impls)
+		constrimpls)
       impls;
   let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in
   if_verbose msg_info (minductive_message warn_prim names);
@@ -639,14 +709,14 @@ type one_inductive_impls =
 let do_mutual_inductive indl poly prv finite =
   let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
-  let mie,impls = interp_mutual_inductive indl ntns poly prv finite in
+  let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in
   (* Declare the mutual inductive block with its associated schemes *)
-  ignore (declare_mutual_inductive_with_eliminations mie impls);
+  ignore (declare_mutual_inductive_with_eliminations mie pl impls);
   (* Declare the possible notations of inductive types *)
   List.iter Metasyntax.add_notation_interpretation ntns;
   (* Declare the coercions *)
   List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes
-
+	    
 (* 3c| Fixpoints and co-fixpoints *)
 
 (* An (unoptimized) function that maps preorders to partial orders...
@@ -697,19 +767,19 @@ let rec partial_order cmp = function
 let non_full_mutual_message x xge y yge isfix rest =
   let reason =
     if Id.List.mem x yge then
-      Id.to_string y^" depends on "^Id.to_string x^" but not conversely"
+      pr_id y ++ str " depends on " ++ pr_id x ++ str " but not conversely"
     else if Id.List.mem y xge then
-      Id.to_string x^" depends on "^Id.to_string y^" but not conversely"
+      pr_id x ++ str " depends on " ++ pr_id y ++ str " but not conversely"
     else
-      Id.to_string y^" and "^Id.to_string x^" are not mutually dependent" in
-  let e = if List.is_empty rest then reason else "e.g.: "^reason in
+      pr_id y ++ str " and " ++ pr_id x ++ str " are not mutually dependent" in
+  let e = if List.is_empty rest then reason else str "e.g., " ++ reason in
   let k = if isfix then "fixpoint" else "cofixpoint" in
   let w =
     if isfix
-    then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl()
+    then str "Well-foundedness check may fail unexpectedly." ++ fnl()
     else mt () in
-  strbrk ("Not a fully mutually defined "^k) ++ fnl () ++
-  strbrk ("("^e^").") ++ fnl () ++ w
+  str "Not a fully mutually defined " ++ str k ++ fnl () ++
+  str "(" ++ e ++ str ")." ++ fnl () ++ w
 
 let check_mutuality env isfix fixl =
   let names = List.map fst fixl in
@@ -725,6 +795,7 @@ let check_mutuality env isfix fixl =
 
 type structured_fixpoint_expr = {
   fix_name : Id.t;
+  fix_univs : lident list option;
   fix_annot : Id.t Loc.located option;
   fix_binders : local_binder list;
   fix_body : constr_expr option;
@@ -734,7 +805,7 @@ type structured_fixpoint_expr = {
 let interp_fix_context env evdref isfix fix =
   let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
   let impl_env, ((env', ctx), imps) = interp_context_evars env evdref before in
-  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env env' evdref after in
+  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(List.length before) env' evdref after in
   let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
     ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
@@ -749,11 +820,12 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
-  declare_definition f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
+  declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
 
-let _ = Obligations.declare_fix_ref := declare_fix
+let _ = Obligations.declare_fix_ref :=
+	  (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps)
 
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -848,7 +920,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   let binders_env = push_rel_context binders_rel env in
   let rel, _ = interp_constr_evars_impls env evdref r in
   let () = check_evars_are_solved env !evdref (Evd.empty,!evdref)  in
-  let relty = Typing.type_of env !evdref rel in
+  let relty = Typing.unsafe_type_of env !evdref rel in
   let relargty =
     let error () =
       user_err_loc (constr_loc r,
@@ -941,7 +1013,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
       let hook l gr = 
 	let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
-	let univs = Evd.universe_context !evdref in
+	let pl, univs = Evd.universe_context !evdref in
 	  (*FIXME poly? *)
 	let ce = definition_entry ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
 	(** FIXME: include locality *)
@@ -975,7 +1047,17 @@ let interp_recursive isfix fixl notations =
   let fixnames = List.map (fun fix -> fix.fix_name) fixl in
 
   (* Interp arities allowing for unresolved types *)
-  let evdref = ref (Evd.from_env env) in
+  let all_universes =
+    List.fold_right (fun sfe acc ->
+        match sfe.fix_univs , acc with
+        | None , acc -> acc
+        | x , None -> x
+        | Some ls , Some us ->
+	   if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then
+	     error "(co)-recursive definitions should all have the same universe binders";
+	   Some (ls @ us)) fixl None in
+  let ctx = Evd.make_evar_universe_context env all_universes in
+  let evdref = ref (Evd.from_ctx ctx) in
   let fixctxs, fiximppairs, fixannots =
     List.split3 (List.map (interp_fix_context env evdref isfix) fixl) in
   let fixctximpenvs, fixctximps = List.split fiximppairs in
@@ -989,7 +1071,7 @@ let interp_recursive isfix fixl notations =
     List.fold_left2
       (fun env' id t ->
 	 if Flags.is_program_mode () then
-	   let sort = Evarutil.evd_comb1 (Typing.e_type_of ~refresh:true env) evdref t in
+	   let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in
 	   let fixprot =
 	     try 
 	       let app = mkApp (delayed_force fix_proto, [|sort; t|]) in
@@ -1022,7 +1104,7 @@ let interp_recursive isfix fixl notations =
   let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in
 
   (* Build the fix declaration block *)
-  (env,rec_sign,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots
+  (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots
 
 let check_recursive isfix env evd (fixnames,fixdefs,_) =
   check_evars_are_solved env evd (Evd.empty,evd);
@@ -1032,16 +1114,16 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) =
   end
 
 let interp_fixpoint l ntns =
-  let (env,_,evd),fix,info = interp_recursive true l ntns in
+  let (env,_,pl,evd),fix,info = interp_recursive true l ntns in
   check_recursive true env evd fix;
-  (fix,Evd.evar_universe_context evd,info)
+  (fix,pl,Evd.evar_universe_context evd,info)
 
 let interp_cofixpoint l ntns =
-  let (env,_,evd),fix,info = interp_recursive false l ntns in
+  let (env,_,pl,evd),fix,info = interp_recursive false l ntns in
   check_recursive false  env evd fix;
-  fix,Evd.evar_universe_context evd,info
+  (fix,pl,Evd.evar_universe_context evd,info)
     
-let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns =
+let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1052,7 +1134,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
     let init_tac =
       Option.map (List.map Proofview.V82.tactic) init_tac
     in
-    let evd = Evd.from_env ~ctx Environ.empty_env in
+    let evd = Evd.from_ctx ctx in
     Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
       evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
@@ -1065,11 +1147,11 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
     let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
-    let ctx = Evd.evar_universe_context_set ctx in
-    let ctx = Universes.restrict_universe_context ctx vars in
-    let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
-    let ctx = Univ.ContextSet.to_context ctx in
-    ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx)
+    let evd = Evd.from_ctx ctx in
+    let evd = Evd.restrict_universe_context evd vars in
+    let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
+    let pl, ctx = Evd.universe_context ?names:pl evd in
+    ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
@@ -1077,7 +1159,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
   (* Declare notations *)
   List.iter Metasyntax.add_notation_interpretation ntns
 
-let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns =
+let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1088,19 +1170,21 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns
     let init_tac =
       Option.map (List.map Proofview.V82.tactic) init_tac
     in
-    let evd = Evd.from_env ~ctx Environ.empty_env in
-    Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
+    let evd = Evd.from_ctx ctx in
+      Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
       evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-    let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
+    let vars = Universes.universes_of_constr (List.hd fixdecls) in
+    let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
-    let ctx = Evd.evar_universe_context_set ctx in
-    let ctx = Univ.ContextSet.to_context ctx in
-    ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx) 
+    let evd = Evd.from_ctx ctx in
+    let evd = Evd.restrict_universe_context evd vars in
+    let pl, ctx = Evd.universe_context ?names:pl evd in
+    ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx) 
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
@@ -1116,15 +1200,17 @@ let extract_decreasing_argument limit = function
 
 let extract_fixpoint_components limit l =
   let fixl, ntnl = List.split l in
-  let fixl = List.map (fun ((_,id),ann,bl,typ,def) ->
+  let fixl = List.map (fun (((_,id),pl),ann,bl,typ,def) ->
     let ann = extract_decreasing_argument limit ann in
-      {fix_name = id; fix_annot = ann; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
+      {fix_name = id; fix_annot = ann; fix_univs = pl;
+       fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
   fixl, List.flatten ntnl
 
 let extract_cofixpoint_components l =
   let fixl, ntnl = List.split l in
-  List.map (fun ((_,id),bl,typ,def) ->
-    {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
+  List.map (fun (((_,id),pl),bl,typ,def) ->
+	    {fix_name = id; fix_annot = None; fix_univs = pl;
+	     fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
   List.flatten ntnl
 
 let out_def = function
@@ -1133,7 +1219,7 @@ let out_def = function
 
 let do_program_recursive local p fixkind fixl ntns =
   let isfix = fixkind != Obligations.IsCoFixpoint in
-  let (env, rec_sign, evd), fix, info = 
+  let (env, rec_sign, pl, evd), fix, info = 
     interp_recursive isfix fixl ntns 
   in
     (* Program-specific code *)
@@ -1177,7 +1263,7 @@ let do_program_recursive local p fixkind fixl ntns =
 let do_program_fixpoint local poly l =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
     match g, l with
-    | [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
+    | [(n, CWfRec r)], [((((_,id),_),_,bl,typ,def),ntn)] ->
 	let recarg = 
 	  match n with
 	  | Some n -> mkIdentC (snd n)
@@ -1186,7 +1272,7 @@ let do_program_fixpoint local poly l =
 		(str "Recursive argument required for well-founded fixpoints")
 	in build_wellfounded (id, n, bl, typ, out_def def) r recarg ntn
 	     
-    | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
+    | [(n, CMeasureRec (m, r))], [((((_,id),_),_,bl,typ,def),ntn)] ->
 	build_wellfounded (id, n, bl, typ, out_def def)
 	  (Option.default (CRef (lt_ref,None)) r) m ntn
 	  
@@ -1203,9 +1289,9 @@ let do_fixpoint local poly l =
   if Flags.is_program_mode () then do_program_fixpoint local poly l
   else
     let fixl, ntns = extract_fixpoint_components true l in
-    let fix = interp_fixpoint fixl ntns in
+    let (_, _, _, info as fix) = interp_fixpoint fixl ntns in
     let possible_indexes =
-      List.map compute_possible_guardness_evidences (pi3 fix) in
+      List.map compute_possible_guardness_evidences info in
     declare_fixpoint local poly fix possible_indexes ntns
 
 let do_cofixpoint local poly l =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 3a38e52c..8e2d9c6f 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -20,25 +20,27 @@ open Pfedit
 (** This file is about the interpretation of raw commands into typed
     ones and top-level declaration of the main Gallina objects *)
 
-val do_universe : Id.t Loc.located list -> unit
-val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
+val do_universe : polymorphic -> Id.t Loc.located list -> unit
+val do_constraint : polymorphic ->
+  (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
 
 (** {6 Hooks for Pcoq} *)
 
-val set_declare_definition_hook : (definition_entry -> unit) -> unit
-val get_declare_definition_hook : unit -> (definition_entry -> unit)
+val set_declare_definition_hook : (Safe_typing.private_constants definition_entry -> unit) -> unit
+val get_declare_definition_hook : unit -> (Safe_typing.private_constants definition_entry -> unit)
 
 (** {6 Definitions/Let} *)
 
 val interp_definition :
-  local_binder list -> polymorphic -> red_expr option -> constr_expr ->
-  constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
+  lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr ->
+  constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
+      Universes.universe_binders * Impargs.manual_implicits
 
 val declare_definition : Id.t -> definition_kind ->
-  definition_entry -> Impargs.manual_implicits ->
+  Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
 
-val do_definition : Id.t -> definition_kind ->
+val do_definition : Id.t -> definition_kind -> lident list option ->
   local_binder list -> red_expr option -> constr_expr ->
   constr_expr option -> unit Lemmas.declaration_hook -> unit
 
@@ -52,12 +54,12 @@ val do_definition : Id.t -> definition_kind ->
     nor in a module type and meant to be instantiated. *)
 val declare_assumption : coercion_flag -> assumption_kind -> 
   types Univ.in_universe_context_set ->
-  Impargs.manual_implicits ->
+  Universes.universe_binders -> Impargs.manual_implicits ->
   bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
   global_reference * Univ.Instance.t * bool
 
 val do_assumptions : locality * polymorphic * assumption_object_kind ->
-  Vernacexpr.inline -> simple_binder with_coercion list -> bool
+  Vernacexpr.inline -> (plident list * constr_expr) with_coercion list -> bool
 
 (* val declare_assumptions : variable Loc.located list -> *)
 (*   coercion_flag -> assumption_kind -> types Univ.in_universe_context_set ->  *)
@@ -70,6 +72,7 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
+  ind_univs : lident list option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }
@@ -90,13 +93,13 @@ type one_inductive_impls =
 val interp_mutual_inductive :
   structured_inductive_expr -> decl_notation list -> polymorphic ->
     private_flag -> Decl_kinds.recursivity_kind ->
-    mutual_inductive_entry * one_inductive_impls list
+    mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
 
 (** Registering a mutual inductive definition together with its
    associated schemes *)
 
 val declare_mutual_inductive_with_eliminations :
-  mutual_inductive_entry -> one_inductive_impls list ->
+  mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list ->
   mutual_inductive
 
 (** Entry points for the vernacular commands Inductive and CoInductive *)
@@ -109,6 +112,7 @@ val do_mutual_inductive :
 
 type structured_fixpoint_expr = {
   fix_name : Id.t;
+  fix_univs : lident list option;
   fix_annot : Id.t Loc.located option;
   fix_binders : local_binder list;
   fix_body : constr_expr option;
@@ -133,24 +137,24 @@ type recursive_preentry =
 
 val interp_fixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * Evd.evar_universe_context * 
+    recursive_preentry * lident list option * Evd.evar_universe_context * 
     (Name.t list * Impargs.manual_implicits * int option) list
 
 val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * Evd.evar_universe_context * 
+    recursive_preentry * lident list option * Evd.evar_universe_context * 
     (Name.t list * Impargs.manual_implicits * int option) list
 
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
   locality -> polymorphic ->
-  recursive_preentry * Evd.evar_universe_context * 
+  recursive_preentry * lident list option * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic -> 
-  recursive_preentry * Evd.evar_universe_context * 
+  recursive_preentry * lident list option * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
 
@@ -166,5 +170,5 @@ val do_cofixpoint :
 
 val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
 
-val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
-  Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
+val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
+  Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index f1d8a492..eca344b2 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -130,10 +130,11 @@ let init_ocaml_path () =
         [ "grammar" ]; [ "ide" ] ]
 
 let get_compat_version = function
+  | "8.5" -> Flags.Current
   | "8.4" -> Flags.V8_4
   | "8.3" -> Flags.V8_3
   | "8.2" -> Flags.V8_2
   | ("8.1" | "8.0") as s ->
-    msg_warning (strbrk ("Compatibility with version "^s^" not supported."));
+    msg_warning (str "Compatibility with version " ++ str s ++ str " not supported.");
     Flags.V8_2
-  | s -> Errors.error ("Unknown compatibility version \""^s^"\".")
+  | s -> Errors.errorlabstrm "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".")
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 52fa9e01..caaf8054 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -176,7 +176,7 @@ let print_location_in_file {outer=s;inner=fname} loc =
     try
       let (line, bol) = line_of_pos 1 0 0 in
       hov 0 (* No line break so as to follow emacs error message format *)
-        (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++
+        (errstrm ++ str"File " ++ str "\"" ++ str fname ++ str "\"" ++
            str", line " ++ int line ++ str", characters " ++
            Cerrors.print_loc (Loc.make_loc (bp-bol,ep-bol))) ++ str":" ++
         fnl ()
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e9e86953..72966a4a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -20,12 +20,6 @@ let () = at_exit flush_all
 
 let ( / ) = Filename.concat
 
-let fatal_error info anomaly =
-  let msg = info ++ fnl () in
-  pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg;
-  flush_all ();
-  exit (if anomaly then 129 else 1)
-
 let get_version_date () =
   try
     let ch = open_in (Envars.coqlib () / "revision") in
@@ -38,7 +32,7 @@ let get_version_date () =
 
 let print_header () =
   let (ver,rev) = get_version_date () in
-  ppnl (str ("Welcome to Coq "^ver^" ("^rev^")"));
+  ppnl (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
   pp_flush ()
 
 let warning s = msg_warning (strbrk s)
@@ -47,8 +41,8 @@ let toploop = ref None
 
 let color : [`ON | `AUTO | `OFF] ref = ref `AUTO
 let set_color = function
-| "on" -> color := `ON
-| "off" -> color := `OFF
+| "yes" | "on" -> color := `ON
+| "no" | "off" -> color := `OFF
 | "auto" -> color := `AUTO
 | _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1
 
@@ -58,7 +52,10 @@ let init_color () =
   | `ON -> true
   | `AUTO ->
     Terminal.has_style Unix.stdout &&
-    Terminal.has_style Unix.stderr
+    Terminal.has_style Unix.stderr &&
+    (* emacs compilation buffer does not support colors by default,
+       its TERM variable is set to "dumb". *)
+    Unix.getenv "TERM" <> "dumb"
   in
   if has_color then begin
     let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
@@ -97,23 +94,43 @@ let output_context = ref false
 let memory_stat = ref false
 
 let print_memory_stat () =
-  if !memory_stat then
+  begin (* -m|--memory from the command-line *)
+    if !memory_stat then
     ppnl
-      (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes")
+      (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes");
+  end;
+  begin
+    (* operf-macro interface:
+       https://github.com/OCamlPro/operf-macro *)
+    try
+      let fn = Sys.getenv "OCAML_GC_STATS" in
+      let oc = open_out fn in
+      Gc.print_stat oc;
+      close_out oc
+    with _ -> ()
+  end
 
 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
 
+let user_warning = ref false
+(** User explicitly set warning *)
+
+let set_warning p =
+  let () = user_warning := true in
+  match p with
+  | "all" -> make_warn true
+  | "none" -> make_warn false
+  | _ -> prerr_endline ("Error: all/none expected after option w"); exit 1
+
 let toplevel_default_name = DirPath.make [Id.of_string "Top"]
 let toplevel_name = ref (Some toplevel_default_name)
 let set_toplevel_name dir =
@@ -127,13 +144,19 @@ let inputstate = ref ""
 let set_inputstate s =
   let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in
   inputstate:=s
-let inputstate () = if not (String.is_empty !inputstate) then intern_state !inputstate
+let inputstate () =
+  if not (String.is_empty !inputstate) then
+    let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in
+    intern_state fname
 
 let outputstate = ref ""
 let set_outputstate s =
   let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in
   outputstate:=s
-let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate
+let outputstate () =
+  if not (String.is_empty !outputstate) then
+    let fname = CUnix.make_suffix !outputstate ".coq" in
+    extern_state fname
 
 let set_include d p implicit =
   let p = dirpath_of_string p in
@@ -145,6 +168,7 @@ let add_load_vernacular verb s =
 let load_vernacular () =
   List.iter
     (fun (s,b) ->
+      let s = Loadpath.locate_file s in
       if Flags.do_beautify () then
 	with_option beautify_file (Vernac.load_vernac b) s
       else
@@ -154,8 +178,8 @@ let load_vernacular () =
 let load_vernacular_obj = ref ([] : string list)
 let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
 let load_vernac_obj () =
-  List.iter (fun f -> Library.require_library_from_file None f None)
-    (List.rev !load_vernacular_obj)
+  let map dir = Qualid (Loc.ghost, qualid_of_string dir) in
+  Vernacentries.vernac_require None None (List.rev_map map !load_vernacular_obj)
 
 let require_prelude () =
   let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in
@@ -168,9 +192,9 @@ let require_prelude () =
 let require_list = ref ([] : string list)
 let add_require s = require_list := s :: !require_list
 let require () =
-  if !load_init then silently require_prelude ();
-  List.iter (fun s -> Library.require_library_from_file None s (Some false))
-    (List.rev !require_list)
+  let () = if !load_init then silently require_prelude () in
+  let map dir = Qualid (Loc.ghost, qualid_of_string dir) in
+  Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list)
 
 let compile_list = ref ([] : (bool * string) list)
 
@@ -209,15 +233,6 @@ let compile_files () =
           compile_file vf)
         (List.rev l)
 
-(*s options for the virtual machine *)
-
-let boxed_val = ref false
-let use_vm = ref false
-
-let set_vm_opt () =
-  Vm.set_transp_values (not !boxed_val);
-  Vconv.set_use_vm !use_vm
-
 (** Options for proof general *)
 
 let set_emacs () =
@@ -276,7 +291,16 @@ let print_style_tags () =
     in
     print_string opt
   in
-  List.iter iter tags;
+  let make (t, st) = match st with
+  | None -> None
+  | Some st ->
+    let tags = List.map string_of_int (Terminal.repr st) in
+    let t = String.concat "." (Ppstyle.repr t) in
+    Some (t ^ "=" ^ String.concat ";" tags)
+  in
+  let repr = List.map_filter make tags in
+  let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in
+  let () = List.iter iter tags in
   flush_all ()
 
 let error_missing_arg s =
@@ -300,8 +324,8 @@ let get_priority opt s =
     prerr_endline ("Error: low/high expected after "^opt); exit 1
 
 let get_async_proofs_mode opt = function
-  | "off" -> Flags.APoff
-  | "on" -> Flags.APon
+  | "no" | "off" -> Flags.APoff
+  | "yes" | "on" -> Flags.APon
   | "lazy" -> Flags.APonLazy
   | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1
 
@@ -315,8 +339,8 @@ let set_worker_id opt s =
   Flags.async_proofs_worker_id := s
 
 let get_bool opt = function
-  | "yes" -> true
-  | "no" -> false
+  | "yes" | "on" -> true
+  | "no" | "off" -> false
   | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1
 
 let get_int opt n =
@@ -326,7 +350,8 @@ let get_int opt n =
 
 let get_host_port opt s =
   match CString.split ':' s with
-  | [host; port] -> Some (Spawned.Socket(host, int_of_string port))
+  | [host; portr; portw] ->
+       Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
   | ["stdfds"] -> Some Spawned.AnonPipe
   | _ ->
      prerr_endline ("Error: host:port or stdfds expected after option "^opt);
@@ -472,6 +497,7 @@ let parse_args arglist =
     |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
     |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
     |"-toploop" -> toploop := Some (next ())
+    |"-w" -> set_warning (next ())
 
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
@@ -481,6 +507,7 @@ let parse_args arglist =
     |"-async-proofs-never-reopen-branch" ->
         Flags.async_proofs_never_reopen_branch := true;
     |"-batch" -> set_batch_mode ()
+    |"-test-mode" -> test_mode := true
     |"-beautify" -> make_beautify true
     |"-boot" -> boot := true; no_load_rc ()
     |"-bt" -> Backtrace.record_backtrace true
@@ -491,18 +518,21 @@ 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
     |"-noinit"|"-nois" -> load_init := false
     |"-no-compat-notations" -> no_compat_ntn := true
     |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
-    |"-no-native-compiler" -> no_native_compiler := true
+    |"-native-compiler" ->
+      if Coq_config.no_native_compiler then
+	warning "Native compilation was disabled at configure time."
+      else native_compiler := true
     |"-notop" -> unset_toplevel_name ()
     |"-output-context" -> output_context := true
     |"-q" -> no_load_rc ()
-    |"-quiet"|"-silent" -> Flags.make_silent true
+    |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false
     |"-quick" -> Flags.compilation_mode := BuildVio
     |"-list-tags" -> print_tags := true
     |"-time" -> Flags.time := true
@@ -510,7 +540,6 @@ let parse_args arglist =
     |"-unicode" -> add_require "Utf8_core"
     |"-v"|"--version" -> Usage.version (exitcode ())
     |"-verbose-compat-notations" -> verb_compat_ntn := true
-    |"-vm" -> use_vm := true
     |"-where" -> print_where := true
 
     (* Deprecated options *)
@@ -570,9 +599,7 @@ let init arglist =
       if_verbose print_header ();
       inputstate ();
       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);
@@ -597,7 +624,8 @@ let init arglist =
         if !batch_mode then mt ()
         else str "Error during initialization:" ++ fnl ()
       in
-      fatal_error (msg ++ Coqloop.print_toplevel_error any) (Errors.is_anomaly (fst any))
+      let is_anomaly e = Errors.is_anomaly e || not (Errors.handled e) in
+      fatal_error (msg ++ Coqloop.print_toplevel_error any) (is_anomaly (fst any))
   end;
   if !batch_mode then begin
     flush_all();
@@ -613,6 +641,7 @@ let start () =
   let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in
   (* In batch mode, Coqtop has already exited at this point. In interactive one,
      dump glob is nothing but garbage ...  *)
+  if not !user_warning then make_warn true;
   !toploop_run ();
   exit 1
 
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 356ccdcc..67044745 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -8,7 +8,7 @@
 
 (** The Coq main module. The following function [start] will parse the
    command line, print the banner, initialize the load path, load the input
-   state, load the files given on the command line, load the ressource file,
+   state, load the files given on the command line, load the resource file,
    produce the output state if any, and finally will launch [Coqloop.loop]. *)
 
 val init_toplevel : string list -> unit
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 7d5d61fb..b6da21e5 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -20,8 +20,8 @@ open Cooking
 (* Discharging mutual inductive *)
 
 let detype_param = function
-  | (Name id,None,p) -> id, Entries.LocalAssum p
-  | (Name id,Some p,_) -> id, Entries.LocalDef p
+  | (Name id,None,p) -> id, LocalAssum p
+  | (Name id,Some p,_) -> id, LocalDef p
   | (Anonymous,_,_) -> anomaly (Pp.str "Unnamed inductive local variable")
 
 (* Replace
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 5429e660..8f380830 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -783,7 +783,7 @@ let explain_pretype_error env sigma err =
     let {uj_val = c; uj_type = actty} = j in
     let (env, c, actty, expty), e = contract3' env c actty t e in
     let j = {uj_val = c; uj_type = actty} in
-    explain_actual_type env sigma j t (Some e)
+    explain_actual_type env sigma j expty (Some e)
   | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs
   | UnsolvableImplicit (evk,exp) -> explain_unsolvable_implicit env sigma evk exp
   | VarNotFound id -> explain_var_not_found env id
@@ -872,11 +872,11 @@ let explain_not_match_error = function
       quote (Univ.pr_constraints (Evd.pr_evd_level Evd.empty) cst)
 
 let explain_signature_mismatch l spec why =
-  str "Signature components for label " ++ str (Label.to_string l) ++
+  str "Signature components for label " ++ pr_label l ++
   str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "."
 
 let explain_label_already_declared l =
-  str ("The label "^Label.to_string l^" is already declared.")
+  str "The label " ++ pr_label l ++ str " is already declared."
 
 let explain_application_to_not_path _ =
   strbrk "A module cannot be applied to another module application or " ++
@@ -924,9 +924,6 @@ let explain_label_missing l s =
   str "The field " ++ str (Label.to_string l) ++ str " is missing in "
   ++ str s ++ str "."
 
-let explain_higher_order_include () =
-  str "You cannot Include a higher-order structure."
-
 let explain_module_error = function
   | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err
   | LabelAlreadyDeclared l -> explain_label_already_declared l
@@ -943,7 +940,6 @@ let explain_module_error = function
   | IncorrectWithConstraint l -> explain_incorrect_label_constraint l
   | GenerativeModuleExpected l -> explain_generative_module_expected l
   | LabelMissing (l,s) -> explain_label_missing l s
-  | HigherOrderInclude -> explain_higher_order_include ()
 
 (* Module internalization errors *)
 
@@ -1086,7 +1082,7 @@ let error_bad_ind_parameters env c n v1 v2  =
   let pv1 = pr_lconstr_env env Evd.empty v1 in
   let pv2 = pr_lconstr_env env Evd.empty v2 in
   str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++
-  str " as " ++ pr_nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "."
+  str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "."
 
 let error_same_names_types id =
   str "The name" ++ spc () ++ pr_id id ++ spc () ++
@@ -1170,18 +1166,18 @@ let explain_bad_constructor env cstr ind =
   str "is expected."
 
 let decline_string n s =
-  if Int.equal n 0 then "no "^s^"s"
-  else if Int.equal n 1 then "1 "^s
-  else (string_of_int n^" "^s^"s")
+  if Int.equal n 0 then str "no " ++ str s ++ str "s"
+  else if Int.equal n 1 then str "1 " ++ str s
+  else (int n ++ str " " ++ str s ++ str "s")
 
 let explain_wrong_numarg_constructor env cstr n =
   str "The constructor " ++ pr_constructor env cstr ++
   str " (in type " ++ pr_inductive env (inductive_of_constructor cstr) ++
-  str ") expects " ++ str (decline_string n "argument") ++ str "."
+  str ") expects " ++ decline_string n "argument" ++ str "."
 
 let explain_wrong_numarg_inductive env ind n =
   str "The inductive type " ++ pr_inductive env ind ++
-  str " expects " ++ str (decline_string n "argument") ++ str "."
+  str " expects " ++ decline_string n "argument" ++ str "."
 
 let explain_unused_clause env pats =
 (* Without localisation
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 138e5189..dde801a7 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -23,15 +23,15 @@ open Util
 open Declare
 open Entries
 open Decl_kinds
+open Pp
 
 (**********************************************************************)
 (* Registering schemes in the environment *)
 
-
 type mutual_scheme_object_function =
-  mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
 type individual_scheme_object_function =
-  inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
 
 type 'a scheme_kind = string
 
@@ -87,7 +87,8 @@ let declare_scheme_object s aux f =
   try
     let _ = Hashtbl.find scheme_object_table key in
 (*    let aux_msg = if aux="" then "" else " (with key "^aux^")" in*)
-    error ("Scheme object "^key^" already declared.")
+    errorlabstrm "IndTables.declare_scheme_object"
+      (str "Scheme object " ++ str key ++ str " already declared.")
   with Not_found ->
     Hashtbl.add scheme_object_table key (s,f);
     key
@@ -112,8 +113,8 @@ let is_visible_name id =
 
 let compute_name internal id =
   match internal with
-  | KernelVerbose | UserVerbose -> id
-  | KernelSilent ->
+  | UserAutomaticRequest | UserIndividualRequest -> id
+  | InternalTacticRequest ->
       Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
 
 let define internal id c p univs =
@@ -123,7 +124,9 @@ let define internal id c p univs =
   let c = Vars.subst_univs_fn_constr 
     (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
   let entry = {
-    const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff);
+    const_entry_body =
+      Future.from_val ((c,Univ.ContextSet.empty),
+                       Safe_typing.empty_private_constants);
     const_entry_secctx = None;
     const_entry_type = None;
     const_entry_polymorphic = p;
@@ -134,66 +137,65 @@ let define internal id c p univs =
   } in
   let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
   let () = match internal with
-    | KernelSilent -> ()
+    | InternalTacticRequest -> ()
     | _-> definition_message id
   in
   kn
 
-let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
-  let (c, ctx), eff = f ind in
+let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
+  let (c, ctx), eff = f mode ind in
   let mib = Global.lookup_mind mind in
   let id = match idopt with
     | Some id -> id
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
-  let const = define internal id c mib.mind_polymorphic ctx in
+  let const = define mode id c mib.mind_polymorphic ctx in
   declare_scheme kind [|ind,const|];
-  const, Declareops.cons_side_effects
-     (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff
+  const, Safe_typing.add_private
+     (Safe_typing.private_con_of_scheme kind (Global.safe_env()) [ind,const]) eff
 
-let define_individual_scheme kind internal names (mind,i as ind) =
+let define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
   | _,MutualSchemeFunction f -> assert false
   | s,IndividualSchemeFunction f ->
-      define_individual_scheme_base kind s f internal names ind
+      define_individual_scheme_base kind s f mode names ind
 
-let define_mutual_scheme_base kind suff f internal names mind =
-  let (cl, ctx), eff = f mind in
+let define_mutual_scheme_base kind suff f mode names mind =
+  let (cl, ctx), eff = f mode mind in
   let mib = Global.lookup_mind mind in
   let ids = Array.init (Array.length mib.mind_packets) (fun i ->
       try Int.List.assoc i names
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
-
   let consts = Array.map2 (fun id cl -> 
-     define internal id cl mib.mind_polymorphic ctx) ids cl in
+     define mode id cl mib.mind_polymorphic ctx) ids cl in
   let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
   declare_scheme kind schemes;
   consts,
-  Declareops.cons_side_effects 
-    (Safe_typing.sideff_of_scheme
+  Safe_typing.add_private 
+    (Safe_typing.private_con_of_scheme
       kind (Global.safe_env()) (Array.to_list schemes))
     eff 
 
-let define_mutual_scheme kind internal names mind =
+let define_mutual_scheme kind mode names mind =
   match Hashtbl.find scheme_object_table kind with
   | _,IndividualSchemeFunction _ -> assert false
   | s,MutualSchemeFunction f ->
-      define_mutual_scheme_base kind s f internal names mind
+      define_mutual_scheme_base kind s f mode names mind
 
 let find_scheme_on_env_too kind ind =
   let s = String.Map.find kind (Indmap.find ind !scheme_map) in
-  s, Declareops.cons_side_effects
-      (Safe_typing.sideff_of_scheme
+  s, Safe_typing.add_private
+      (Safe_typing.private_con_of_scheme
             kind (Global.safe_env()) [ind, s])
-      Declareops.no_seff 
+      Safe_typing.empty_private_constants
 
-let find_scheme kind (mind,i as ind) =
+let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
   try find_scheme_on_env_too kind ind
   with Not_found ->
   match Hashtbl.find scheme_object_table kind with
   | s,IndividualSchemeFunction f ->
-      define_individual_scheme_base kind s f KernelSilent None ind
+      define_individual_scheme_base kind s f mode None ind
   | s,MutualSchemeFunction f ->
-      let ca, eff = define_mutual_scheme_base kind s f KernelSilent [] mind in
+      let ca, eff = define_mutual_scheme_base kind s f mode [] mind in
       ca.(i), eff
 
 let check_scheme kind ind =
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index 98eaac09..abd951c3 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -8,6 +8,7 @@
 
 open Term
 open Names
+open Declare
 
 (** This module provides support for registering inductive scheme builders,
    declaring schemes and generating schemes on demand *)
@@ -19,9 +20,9 @@ type individual
 type 'a scheme_kind
 
 type mutual_scheme_object_function =
-  mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
 type individual_scheme_object_function =
-  inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
 
 (** Main functions to register a scheme builder *)
 
@@ -32,21 +33,17 @@ val declare_individual_scheme_object : string -> ?aux:string ->
   individual_scheme_object_function ->
   individual scheme_kind
 
-(*
-val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit
-*)
-
 (** Force generation of a (mutually) scheme with possibly user-level names *)
 
 val define_individual_scheme : individual scheme_kind -> 
-  Declare.internal_flag (** internal *) ->
-  Id.t option -> inductive -> constant * Declareops.side_effects
+  internal_flag (** internal *) ->
+  Id.t option -> inductive -> constant * Safe_typing.private_constants
 
-val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) ->
-  (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects
+val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
+  (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants
 
 (** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : 'a scheme_kind -> inductive -> constant * Declareops.side_effects
+val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants
 
 val check_scheme : 'a scheme_kind -> inductive -> bool
 
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index fbc45b4a..f16e6e3f 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -129,7 +129,7 @@ let define id internal ctx c t =
         const_entry_secctx = None;
         const_entry_type = t;
 	const_entry_polymorphic = true;
-	const_entry_universes = Evd.universe_context ctx;
+	const_entry_universes = snd (Evd.universe_context ctx);
         const_entry_opaque = false;
         const_entry_inline_code = false;
         const_entry_feedback = None;
@@ -146,8 +146,8 @@ let declare_beq_scheme_gen internal names kn =
 let alarm what internal msg =
   let debug = false in
   match internal with
-  | KernelVerbose 
-  | KernelSilent ->
+  | UserAutomaticRequest
+  | InternalTacticRequest ->
     (if debug then
       msg_warning
 	(hov 0 msg ++ fnl () ++ what ++ str " not defined."))
@@ -180,10 +180,12 @@ let try_declare_scheme what f internal names kn =
 	  (strbrk "Required constant " ++ str s ++ str " undefined.")
     | AlreadyDeclared msg ->
         alarm what internal (msg ++ str ".")
+    | DecidabilityMutualNotSupported ->
+        alarm what internal
+          (str "Decidability lemma for mutual inductive types not supported.")
     | e when Errors.noncritical e ->
-	alarm what internal
-	  (str "Unknown exception during scheme creation: "++
-           str (Printexc.to_string e))
+        alarm what internal
+	  (str "Unexpected error during scheme creation: " ++ Errors.print e)
 
 let beq_scheme_msg mind =
   let mib = Global.lookup_mind mind in
@@ -193,13 +195,13 @@ let beq_scheme_msg mind =
     (List.init (Array.length mib.mind_packets) (fun i -> (mind,i)))
 
 let declare_beq_scheme_with l kn =
-  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserIndividualRequest l kn
 
 let try_declare_beq_scheme kn =
   (* TODO: handle Fix, eventually handle
       proof-irrelevance; improve decidability by depending on decidability
       for the parameters rather than on the bl and lb properties *)
-  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelVerbose [] kn
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserAutomaticRequest [] kn
 
 let declare_beq_scheme = declare_beq_scheme_with []
 
@@ -213,7 +215,7 @@ let declare_one_case_analysis_scheme ind =
        induction scheme, the other ones share the same code with the
        apropriate type *)
   if Sorts.List.mem InType kelim then
-    ignore (define_individual_scheme dep KernelVerbose None ind)
+    ignore (define_individual_scheme dep UserAutomaticRequest None ind)
 
 (* Induction/recursion schemes *)
 
@@ -236,7 +238,7 @@ let declare_one_induction_scheme ind =
     List.map_filter (fun (sort,kind) ->
       if Sorts.List.mem sort kelim then Some kind else None)
       (if from_prop then kinds_from_prop else kinds_from_type) in
-  List.iter (fun kind -> ignore (define_individual_scheme kind KernelVerbose None ind))
+  List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
     elims
 
 let declare_induction_schemes kn =
@@ -259,11 +261,11 @@ let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
 
 let declare_eq_decidability_scheme_with l kn =
   try_declare_scheme (eq_dec_scheme_msg (kn,0))
-    declare_eq_decidability_gen UserVerbose l kn
+    declare_eq_decidability_gen UserIndividualRequest l kn
 
 let try_declare_eq_decidability kn =
   try_declare_scheme (eq_dec_scheme_msg (kn,0))
-    declare_eq_decidability_gen KernelVerbose [] kn
+    declare_eq_decidability_gen UserAutomaticRequest [] kn
 
 let declare_eq_decidability = declare_eq_decidability_scheme_with []
 
@@ -272,17 +274,17 @@ let ignore_error f x =
 
 let declare_rewriting_schemes ind =
   if Hipattern.is_inductive_equality ind then begin
-    ignore (define_individual_scheme rew_r2l_scheme_kind KernelVerbose None ind);
-    ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelVerbose None ind);
+    ignore (define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind);
+    ignore (define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind);
     ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
-      KernelVerbose None ind);
+      UserAutomaticRequest None ind);
     (* These ones expect the equality to be symmetric; the first one also *)
     (* needs eq *)
-    ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelVerbose None) ind;
+    ignore_error (define_individual_scheme rew_l2r_scheme_kind UserAutomaticRequest None) ind;
     ignore_error
-      (define_individual_scheme rew_l2r_dep_scheme_kind KernelVerbose None) ind;
+      (define_individual_scheme rew_l2r_dep_scheme_kind UserAutomaticRequest None) ind;
     ignore_error
-      (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelVerbose None) ind
+      (define_individual_scheme rew_l2r_forward_dep_scheme_kind UserAutomaticRequest None) ind
   end
 
 let declare_congr_scheme ind =
@@ -291,7 +293,7 @@ let declare_congr_scheme ind =
       try Coqlib.check_required_library Coqlib.logic_module_name; true
       with e when Errors.noncritical e -> false
     then
-      ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind)
+      ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
     else
       msg_warning (strbrk "Cannot build congruence scheme because eq is not found")
   end
@@ -299,7 +301,7 @@ let declare_congr_scheme ind =
 let declare_sym_scheme ind =
   if Hipattern.is_inductive_equality ind then
     (* Expect the equality to be symmetric *)
-    ignore_error (define_individual_scheme sym_scheme_kind KernelVerbose None) ind
+    ignore_error (define_individual_scheme sym_scheme_kind UserAutomaticRequest None) ind
 
 (* Scheme command *)
 
@@ -369,8 +371,8 @@ let do_mutual_induction_scheme lnamedepindsort =
   let declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 sigma decl in
     (* let decltype = refresh_universes decltype in *)
-    let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Declareops.no_seff) in
-    let cst = define fi UserVerbose sigma proof_output (Some decltype) in
+    let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+    let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in
     ConstRef cst :: lrecref
   in
   let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -421,7 +423,7 @@ let fold_left' f = function
 
 let build_combined_scheme env schemes =
   let defs = List.map (fun cst -> (* FIXME *)
-    let evd, c = Evd.fresh_constant_instance env Evd.empty cst in
+    let evd, c = Evd.fresh_constant_instance env (Evd.from_env env) cst in
       (c, Typeops.type_of_constant_in env c)) schemes in
 (*   let nschemes = List.length schemes in *)
   let find_inductive ty =
@@ -467,8 +469,8 @@ let do_combined_scheme name schemes =
       schemes
   in
   let body,typ = build_combined_scheme (Global.env ()) csts in
-  let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Declareops.no_seff) in
-  ignore (define (snd name) UserVerbose Evd.empty proof_output (Some typ));
+  let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+  ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ));
   fixpoint_message None [snd name]
 
 (**********************************************************************)
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index f711dad9..1145a20b 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
+
 (** * Managing locality *)
 
 let local_of_bool = function
@@ -16,7 +18,8 @@ let check_locality locality_flag =
   match locality_flag with
   | Some b ->
     let s = if b then "Local" else "Global" in
-    Errors.error ("This command does not support the \""^s^"\" prefix.")
+    Errors.errorlabstrm "Locality.check_locality"
+      (str "This command does not support the \"" ++ str s ++ str "\" prefix.")
   | None -> ()
 
 (** Extracting the locality flag *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 639ec1e6..7616bfff 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -84,8 +84,14 @@ type tactic_grammar_obj = {
   tacobj_body : Tacexpr.glob_tactic_expr
 }
 
+let check_key key =
+  if Tacenv.check_alias key then
+    error "Conflicting tactic notations keys. This can happen when including \
+    twice the same module."
+
 let cache_tactic_notation (_, tobj) =
   let key = tobj.tacobj_key in
+  let () = check_key key in
   Tacenv.register_alias key tobj.tacobj_body;
   Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
@@ -97,6 +103,7 @@ let open_tactic_notation i (_, tobj) =
 
 let load_tactic_notation i (_, tobj) =
   let key = tobj.tacobj_key in
+  let () = check_key key in
   (** Only add the printing and interpretation rules. *)
   Tacenv.register_alias key tobj.tacobj_body;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
@@ -387,7 +394,8 @@ let rec find_pattern nt xl = function
   | _, Break s :: _ | Break s :: _, _ ->
       error ("A break occurs on one side of \"..\" but not on the other side.")
   | _, Terminal s :: _ | Terminal s :: _, _ ->
-      error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.")
+      errorlabstrm "Metasyntax.find_pattern"
+        (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.")
   | _, [] ->
       error msg_expected_form_of_recursive_notation
   | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
@@ -448,7 +456,8 @@ let rec get_notation_vars = function
       let vars = get_notation_vars sl in
       if Id.equal id ldots_var then vars else
 	if Id.List.mem id vars then
-	  error ("Variable "^Id.to_string id^" occurs more than once.")
+	  errorlabstrm "Metasyntax.get_notation_vars"
+            (str "Variable " ++ pr_id id ++ str " occurs more than once.")
 	else
           id::vars
   | (Terminal _ | Break _) :: sl -> get_notation_vars sl
@@ -461,8 +470,8 @@ let analyze_notation_tokens l =
   recvars, List.subtract Id.equal vars (List.map snd recvars), l
 
 let error_not_same_scope x y =
-  error ("Variables "^Id.to_string x^" and "^Id.to_string y^
-    " must be in the same scope.")
+  errorlabstrm "Metasyntax.error_not_name_scope"
+    (str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.")
 
 (**********************************************************************)
 (* Build pretty-printing rules                                        *)
@@ -710,7 +719,7 @@ let is_not_small_constr = function
 let rec define_keywords_aux = function
   | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
       when is_not_small_constr e ->
-      Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
+      Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
       Lexer.add_keyword k;
       n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | n :: l -> n :: define_keywords_aux l
@@ -719,7 +728,7 @@ let rec define_keywords_aux = function
   (* Ensure that IDENT articulation terminal symbols are keywords *)
 let define_keywords = function
   | GramConstrTerminal(IDENT k)::l ->
-      Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
+      Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
       Lexer.add_keyword k;
       GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | l -> define_keywords_aux l
@@ -804,7 +813,7 @@ let pr_level ntn (from,args) =
 
 let error_incompatible_level ntn oldprec prec =
   errorlabstrm ""
-    (str ("Notation "^ntn^" is already defined") ++ spc() ++
+    (str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++
     pr_level ntn oldprec ++
     spc() ++ str "while it is now required to be" ++ spc() ++
     pr_level ntn prec ++ str ".")
@@ -871,14 +880,16 @@ let interp_modifiers modl =
     | SetEntryType (s,typ) :: l ->
 	let id = Id.of_string s in
 	if Id.List.mem_assoc id etyps then
-	  error (s^" is already assigned to an entry or constr level.");
+	  errorlabstrm "Metasyntax.interp_modifiers"
+            (str s ++ str " is already assigned to an entry or constr level.");
 	interp assoc level ((id,typ)::etyps) format extra l
     | SetItemLevel ([],n) :: l ->
 	interp assoc level etyps format extra l
     | SetItemLevel (s::idl,n) :: l ->
 	let id = Id.of_string s in
 	if Id.List.mem_assoc id etyps then
-	  error (s^" is already assigned to an entry or constr level.");
+	  errorlabstrm "Metasyntax.interp_modifiers"
+            (str s ++ str " is already assigned to an entry or constr level.");
 	let typ = ETConstr (n,()) in
 	interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l)
     | SetLevel n :: l ->
@@ -905,7 +916,8 @@ let check_infix_modifiers modifiers =
 let check_useless_entry_types recvars mainvars etyps =
   let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in
   match List.filter (fun (x,etyp) -> not (List.mem x vars)) etyps with
-  | (x,_)::_ -> error (Id.to_string x ^ " is unbound in the notation.")
+  | (x,_)::_ -> errorlabstrm "Metasyntax.check_useless_entry_types"
+                  (pr_id x ++ str " is unbound in the notation.")
   | _ -> ()
 
 let no_syntax_modifiers = function
@@ -1371,7 +1383,10 @@ let add_infix local ((loc,inf),modifiers) pr sc =
 (**********************************************************************)
 (* Delimiters and classes bound to scopes                             *)
 
-type scope_command = ScopeDelim of string | ScopeClasses of scope_class list
+type scope_command =
+  | ScopeDelim of string
+  | ScopeClasses of scope_class list
+  | ScopeRemove
 
 let load_scope_command _ (_,(scope,dlm)) =
   Notation.declare_scope scope
@@ -1381,6 +1396,7 @@ let open_scope_command i (_,(scope,o)) =
     match o with
     | ScopeDelim dlm -> Notation.declare_delimiters scope dlm
     | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl
+    | ScopeRemove -> Notation.remove_delimiters scope
 
 let cache_scope_command o =
   load_scope_command 1 o;
@@ -1406,6 +1422,9 @@ let inScopeCommand : scope_name * scope_command -> obj =
 let add_delimiters scope key =
   Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key))
 
+let remove_delimiters scope =
+  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove))
+
 let add_class_scope scope cl =
   Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl))
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 38a37757..f22839f4 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -39,6 +39,7 @@ val add_notation_extra_printing_rule : string -> string -> string -> unit
 (** Declaring delimiter keys and default scopes *)
 
 val add_delimiters : scope_name -> string -> unit
+val remove_delimiters : scope_name -> unit
 val add_class_scope : scope_name -> scope_class list -> unit
 
 (** Add only the interpretation of a notation that already has pa/pp rules *)
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 0b6fc48c..a7fb7a58 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -164,7 +164,7 @@ let add_rec_ml_dir unix_path =
 let convert_string d =
   try Names.Id.of_string d
   with UserError _ ->
-    msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
+    msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
     raise Exit
 
 let add_rec_path ~unix_path ~coq_root ~implicit =
@@ -184,7 +184,7 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
     let () = List.iter add dirs in
     Loadpath.add_load_path unix_path ~implicit coq_root
   else
-    msg_warning (str ("Cannot open " ^ unix_path))
+    msg_warning (str "Cannot open " ++ str unix_path)
 
 (* convertit un nom quelconque en nom de fichier ou de module *)
 let mod_of_name name =
@@ -321,13 +321,13 @@ let reset_loaded_modules () = loaded_modules := []
 let if_verbose_load verb f name ?path fname =
   if not verb then f name ?path fname
   else
-    let info = "[Loading ML file "^fname^" ..." in
+    let info = str "[Loading ML file " ++ str fname ++ str " ..." in
     try
       let path = f name ?path fname in
-      msg_info (str (info^" done]"));
+      msg_info (info ++ str " done]");
       path
     with reraise ->
-      msg_info (str (info^" failed]"));
+      msg_info (info ++ str " failed]");
       raise reraise
 
 (** Load a module for the first time (i.e. dynlink it)
@@ -340,7 +340,8 @@ let trigger_ml_object verb cache reinit ?path name =
     add_loaded_module name (known_module_path name);
     if cache then perform_cache_obj name
   end else if not has_dynlink then
-    error ("Dynamic link not supported (module "^name^")")
+    errorlabstrm "Mltop.trigger_ml_object"
+      (str "Dynamic link not supported (module " ++ str name ++ str ")")
   else begin
     let file = file_of_name (Option.default name path) in
     let path =
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 523134b5..9019f486 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -306,7 +306,7 @@ type fixpoint_kind =
 
 type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
 
-type program_info = {
+type program_info_aux = {
   prg_name: Id.t;
   prg_body: constr;
   prg_type: constr;
@@ -322,6 +322,13 @@ type program_info = {
   prg_opaque : bool;
 }
 
+type program_info = program_info_aux Ephemeron.key
+
+let get_info x =
+  try Ephemeron.get x
+  with Ephemeron.InvalidKey ->
+    Errors.anomaly Pp.(str "Program obligation can't be accessed by a worker")
+
 let assumption_message = Declare.assumption_message
 
 let (set_default_tactic, get_default_tactic, print_default_tactic) = 
@@ -452,23 +459,10 @@ let subst_deps_obl obls obl =
 
 module ProgMap = Map.Make(Id)
 
-let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)
+let map_replace k v m = ProgMap.add k (Ephemeron.create v) (ProgMap.remove k m)
 
 let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
 
-let map_cardinal m =
-  let i = ref 0 in
-    ProgMap.iter (fun _ _ -> incr i) m;
-    !i
-
-exception Found of program_info
-
-let map_first m =
-  try
-    ProgMap.iter (fun _ v -> raise (Found v)) m;
-    assert(false)
-  with Found x -> x
-
 let from_prg : program_info ProgMap.t ref =
   Summary.ref ProgMap.empty ~name:"program-tcc-table"
 
@@ -514,16 +508,17 @@ let declare_definition prg =
   let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
     (Evd.evar_universe_context_subst prg.prg_ctx) in
   let opaque = prg.prg_opaque in
+  let fix_exn = Stm.get_fix_exn () in
   let ce =
-    definition_entry ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
-      ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
+    definition_entry ~fix_exn
+     ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
+     ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
   in
     progmap_remove prg;
     !declare_definition_ref prg.prg_name 
       prg.prg_kind ce prg.prg_implicits
-      (Lemmas.mk_hook (fun l r ->
-         Lemmas.call_hook (fun exn -> exn) prg.prg_hook l r; r))
-
+      (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r; r))
+      
 open Pp
 
 let rec lam_index n t acc =
@@ -547,7 +542,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
       let ctx = fst (decompose_prod_n_assum m fixtype) in
 	List.map_i (fun i _ -> i) 0 ctx
 
-let mk_proof c = ((c, Univ.ContextSet.empty), Declareops.no_seff)
+let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants)
 
 let declare_mutual_definition l =
   let len = List.length l in
@@ -606,12 +601,17 @@ let shrink_body c =
       else mkLambda (n,t,b), succ i, mkRel i :: args)
      (b, 1, []) ctx
   in List.map (fun (c,t) -> (c,None,t)) ctx, b', Array.of_list args
-      
+
+let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
+
+let add_hint local prg cst =
+  Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst)
+
 let declare_obligation prg obl body ty uctx =
   let body = prg.prg_reduce body in
   let ty = Option.map prg.prg_reduce ty in
   match obl.obl_status with
-  | Evar_kinds.Expand -> { obl with obl_body = Some (TermObl body) }
+  | Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) }
   | Evar_kinds.Define opaque ->
       let opaque = if get_proofs_transparency () then false else opaque in
       let poly = pi2 prg.prg_kind in
@@ -619,8 +619,9 @@ let declare_obligation prg obl body ty uctx =
 	if get_shrink_obligations () && not poly then
 	  shrink_body body else [], body, [||] 
       in
+      let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
       let ce = 
-        { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff);
+        { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
           const_entry_secctx = None;
 	  const_entry_type = if List.is_empty ctx then ty else None;
 	  const_entry_polymorphic = poly;
@@ -633,11 +634,9 @@ let declare_obligation prg obl body ty uctx =
       let constant = Declare.declare_constant obl.obl_name ~local:true
 	(DefinitionEntry ce,IsProof Property)
       in
-	if not opaque then
-	  Hints.add_hints false [Id.to_string prg.prg_name]
-	    (Hints.HintsUnfoldEntry [EvalConstRef constant]);
+	if not opaque then add_hint false prg constant;
 	definition_message obl.obl_name;
-	{ obl with obl_body = 
+	true, { obl with obl_body =
 	    if poly then 
 	      Some (DefinedObl constant)
 	    else
@@ -670,17 +669,33 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls
       prg_hook = hook;
       prg_opaque = opaque; }
 
+let map_cardinal m =
+  let i = ref 0 in
+  ProgMap.iter (fun _ v ->
+		if snd (Ephemeron.get v).prg_obligations > 0 then incr i) m;
+  !i
+
+exception Found of program_info
+
+let map_first m =
+  try
+    ProgMap.iter (fun _ v ->
+		  if snd (Ephemeron.get v).prg_obligations > 0 then
+		    raise (Found v)) m;
+    assert(false)
+  with Found x -> x
+
 let get_prog name =
   let prg_infos = !from_prg in
     match name with
 	Some n ->
-	  (try ProgMap.find n prg_infos
+	  (try get_info (ProgMap.find n prg_infos)
 	   with Not_found -> raise (NoObligations (Some n)))
       | None ->
 	  (let n = map_cardinal prg_infos in
 	     match n with
 		 0 -> raise (NoObligations None)
-	       | 1 -> map_first prg_infos
+	       | 1 -> get_info (map_first prg_infos)
 	       | _ -> 
                    error ("More than one program with unsolved obligations: "^
                     String.concat ", " 
@@ -690,7 +705,7 @@ let get_prog name =
 let get_any_prog () =
   let prg_infos = !from_prg in
   let n = map_cardinal prg_infos in
-  if n > 0 then map_first prg_infos
+  if n > 0 then get_info (map_first prg_infos)
   else raise (NoObligations None)
 
 let get_prog_err n =
@@ -730,7 +745,7 @@ let update_obls prg obls rem =
 	    progmap_remove prg';
 	    Defined kn
       | l ->
-	  let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
+	  let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in
 	    if List.for_all (fun x -> obligations_solved x) progs then
 	      let kn = declare_mutual_definition progs in
 		Defined (ConstRef kn)
@@ -767,7 +782,7 @@ let not_transp_msg =
   str "Obligation should be transparent but was declared opaque." ++ spc () ++
     str"Use 'Defined' instead."
 
-let error_not_transp () = pperror not_transp_msg
+let err_not_transp () = pperror not_transp_msg
 
 let rec string_of_list sep f = function
     [] -> ""
@@ -783,81 +798,68 @@ let solve_by_tac name evi t poly ctx =
   let (entry,_,ctx') = Pfedit.build_constant_by_tactic 
     id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
   let env = Global.env () in
-  let entry = Term_typing.handle_entry_side_effects env entry in
-  let body, eff = Future.force entry.Entries.const_entry_body in
-  assert(Declareops.side_effects_is_empty eff);
-  assert(Univ.ContextSet.is_empty (snd body));
+  let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
+  let body, eff = Future.force entry.const_entry_body in
+  assert(Safe_typing.empty_private_constants = eff);
+  let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
   Inductiveops.control_only_guard (Global.env ()) (fst body);
-  (fst body), entry.Entries.const_entry_type, ctx'
+  (fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
+
+let obligation_hook prg obl num auto ctx' _ gr =
+  let obls, rem = prg.prg_obligations in
+  let cst = match gr with ConstRef cst -> cst | _ -> assert false in
+  let transparent = evaluable_constant cst (Global.env ()) in
+  let () = match obl.obl_status with
+  | Evar_kinds.Expand -> if not transparent then err_not_transp ()
+  | Evar_kinds.Define op -> if not op && not transparent then err_not_transp ()
+  in
+  let obl = { obl with obl_body = Some (DefinedObl cst) } in
+  let () = if transparent then add_hint true prg cst in
+  let obls = Array.copy obls in
+  let _ = obls.(num) <- obl in
+  let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
+  let ctx' =
+    if not (pi2 prg.prg_kind) (* Not polymorphic *) then
+      (* The universe context was declared globally, we continue
+         from the new global environment. *)
+      Evd.evar_universe_context (Evd.from_env (Global.env ()))
+    else ctx'
+  in
+  let prg = { prg with prg_ctx = ctx' } in
+  let () =
+    try ignore (update_obls prg obls (pred rem))
+    with e when Errors.noncritical e ->
+      let e = Errors.push e in
+      pperror (Errors.iprint (Cerrors.process_vernac_interp_error e))
+  in
+  if pred rem > 0 then begin
+    let deps = dependencies obls num in
+    if not (Int.Set.is_empty deps) then
+      ignore (auto (Some prg.prg_name) None deps)
+  end
 
 let rec solve_obligation prg num tac =
   let user_num = succ num in
   let obls, rem = prg.prg_obligations in
   let obl = obls.(num) in
+  let remaining = deps_remaining obls obl.obl_deps in
+  let () =
     if not (Option.is_empty obl.obl_body) then
-      pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")
-    else
-      match deps_remaining obls obl.obl_deps with
-      | [] ->
-          let obl = subst_deps_obl obls obl in
-          let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
-            let evd = Evd.from_env ~ctx:prg.prg_ctx Environ.empty_env in
-            Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type
-              (fun ctx' -> Lemmas.mk_hook (fun strength gr ->
-		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
-		let obl =
-		  let transparent = evaluable_constant cst (Global.env ()) in
-		  let body =
-		    match obl.obl_status with
-		    | Evar_kinds.Expand ->
-			if not transparent then error_not_transp ()
-			else DefinedObl cst
-		    | Evar_kinds.Define opaque ->
-			if not opaque && not transparent then error_not_transp ()
-			else DefinedObl cst
-		  in
-		    if transparent then
-		      Hints.add_hints true [Id.to_string prg.prg_name]
-			(Hints.HintsUnfoldEntry [EvalConstRef cst]);
-		    { obl with obl_body = Some body }
-		in
-		let obls = Array.copy obls in
-		let _ = obls.(num) <- obl in
-		let ctx' = 
-		  let ctx = 
-		    match ctx' with
-		    | None -> prg.prg_ctx
-		    | Some ctx' -> ctx'
-		  in
-  		    if not (pi2 prg.prg_kind) (* Not polymorphic *) then
-		      (* This context is already declared globally, we cannot 
-			 instantiate the rigid variables anymore *) 
-		      Evd.abstract_undefined_variables ctx
-		    else ctx
-		in
-		let res = 
-		  try update_obls 
-			{prg with prg_body = prg.prg_body;
-			  prg_type = prg.prg_type;
-			  prg_ctx = ctx' }
-			  
-			obls (pred rem)
-		  with e when Errors.noncritical e ->
-                    let e = Errors.push e in
-                    pperror (Errors.iprint (Cerrors.process_vernac_interp_error e))
-		in
-		  match res with
-		  | Remain n when n > 0 ->
-		      let deps = dependencies obls num in
-			if not (Int.Set.is_empty deps) then
-			  ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
-		  | _ -> ()));
-	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
-		     Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type);
-	    ignore (Pfedit.by (snd (get_default_tactic ())));
-	    Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
-      | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
-		      ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
+      pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.");
+    if not (List.is_empty remaining) then
+      pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
+        ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining));
+  in
+  let obl = subst_deps_obl obls obl in
+  let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
+  let evd = Evd.from_ctx prg.prg_ctx in
+  let auto n tac oblset = auto_solve_obligations n ~oblset tac in
+  let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
+  let () = Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type hook in
+  let () = trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
+            Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in
+  let _ = Pfedit.by (snd (get_default_tactic ())) in
+  Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
 
 and obligation (user_num, name, typ) tac =
   let num = pred user_num in
@@ -892,8 +894,13 @@ and solve_obligation_by_tac prg obls i tac =
 	        (pi2 !prg.prg_kind) !prg.prg_ctx
 	    in
 	    let uctx = Evd.evar_context_universe_context ctx in
-	      prg := {!prg with prg_ctx = ctx};
-	      obls.(i) <- declare_obligation !prg obl t ty uctx;
+	    let () = prg := {!prg with prg_ctx = ctx} in
+	    let def, obl' = declare_obligation !prg obl t ty uctx in
+	      obls.(i) <- obl';
+	      if def && not (pi2 !prg.prg_kind) then (
+		(* Declare the term constraints with the first obligation only *)
+		let ctx' = Evd.evar_universe_context (Evd.from_env (Global.env ())) in
+		  prg := {!prg with prg_ctx = ctx'});
 	      true
 	  else false
 	with e when Errors.noncritical e ->
@@ -929,7 +936,7 @@ and solve_obligations n tac =
     solve_prg_obligations prg tac
 
 and solve_all_obligations tac =
-  ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg
+  ProgMap.iter (fun k v -> ignore(solve_prg_obligations (get_info v) tac)) !from_prg
 
 and try_solve_obligation n prg tac =
   let prg = get_prog prg in
@@ -970,7 +977,7 @@ let show_obligations ?(msg=true) n =
     | Some n ->
 	try [ProgMap.find n !from_prg]
 	with Not_found -> raise (NoObligations (Some n))
-  in List.iter (show_obligations_of_prg ~msg) progs
+  in List.iter (fun x -> show_obligations_of_prg ~msg (get_info x)) progs
 
 let show_term n =
   let prg = get_prog_err n in
@@ -991,7 +998,7 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
   else (
     let len = Array.length obls in
     let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
-      progmap_add n prg;
+      progmap_add n (Ephemeron.create prg);
       let res = auto_solve_obligations (Some n) tactic in
 	match res with
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
@@ -1004,7 +1011,7 @@ let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduc
     (fun  (n, b, t, imps, obls) ->
      let prg = init_prog_info ~opaque n (Some b) t ctx deps (Some fixkind)
        notations obls imps kind reduce hook 
-     in progmap_add n prg) l;
+     in progmap_add n (Ephemeron.create prg)) l;
     let _defined =
       List.fold_left (fun finished x ->
 	if finished then finished
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 40f124ca..61a8ee52 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -17,11 +17,11 @@ open Decl_kinds
 
 (** Forward declaration. *)
 val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
-  Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
+  Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
 
 val declare_definition_ref :
   (Id.t -> definition_kind ->
-     Entries.definition_entry -> Impargs.manual_implicits
+     Safe_typing.private_constants Entries.definition_entry -> Impargs.manual_implicits
        -> global_reference Lemmas.declaration_hook -> global_reference) ref
 
 val check_evars : env -> evar_map -> unit
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 737b7fb5..dc2c9264 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -90,9 +90,10 @@ let binder_of_decl = function
 
 let binders_of_decls = List.map binder_of_decl
 
-let typecheck_params_and_fields def id t ps nots fs =
+let typecheck_params_and_fields def id pl t ps nots fs =
   let env0 = Global.env () in
-  let evars = ref (Evd.from_env env0) in
+  let ctx = Evd.make_evar_universe_context env0 pl in
+  let evars = ref (Evd.from_ctx ctx) in
   let _ = 
     let error bk (loc, name) = 
       match bk, name with
@@ -130,14 +131,21 @@ let typecheck_params_and_fields def id t ps nots fs =
     Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in
   let evars, nf = Evarutil.nf_evars_and_universes sigma in
   let arity = nf t' in
-  let evars = 
+  let arity, evars = 
     let _, univ = compute_constructor_level evars env_ar newfs in
     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
-	evars
-      else Evd.set_leq_sort env_ar evars (Type univ) aritysort
+	(Sorts.is_set aritysort && is_impredicative_set env0) then
+	arity, evars
+      else
+	let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in
+	  if Univ.is_small_univ univ then
+	    (* We can assume that the level aritysort is not constrained
+  	       and clear it. *)
+	    mkArity (ctx, Sorts.sort_of_univ univ),
+	    Evd.set_eq_sort env_ar evars (Prop Pos) aritysort
+	  else arity, evars
   in
   let evars, nf = Evarutil.nf_evars_and_universes evars in
   let newps = map_rel_context nf newps in
@@ -145,15 +153,15 @@ let typecheck_params_and_fields def id t ps nots fs =
   let ce t = Evarutil.check_evars env0 Evd.empty evars t in
     List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps);
     List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs);
-    Evd.universe_context evars, nf arity, template, imps, newps, impls, newfs
+    Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs
 
 let degenerate_decl (na,b,t) =
   let id = match na with
     | Name id -> id
     | Anonymous -> anomaly (Pp.str "Unnamed record variable") in
   match b with
-    | None -> (id, Entries.LocalAssum t)
-    | Some b -> (id, Entries.LocalDef b)
+    | None -> (id, LocalAssum t)
+    | Some b -> (id, LocalDef b)
 
 type record_error =
   | MissingProj of Id.t * Id.t list
@@ -232,7 +240,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
   let (mib,mip) = Global.lookup_inductive indsp in
   let u = Declareops.inductive_instance mib in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
-  let poly = mib.mind_polymorphic and ctx = Univ.instantiate_univ_context mib.mind_universes in
+  let poly = mib.mind_polymorphic in
+  let ctx = Univ.instantiate_univ_context mib.mind_universes in
   let indu = indsp, u in
   let r = mkIndU (indsp,u) in
   let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in
@@ -288,16 +297,17 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 	        try
 		  let entry = {
 		    const_entry_body =
-		      Future.from_val (Term_typing.mk_pure_proof proj);
+		      Future.from_val (Safe_typing.mk_pure_proof proj);
 		    const_entry_secctx = None;
 		    const_entry_type = Some projtyp;
 		    const_entry_polymorphic = poly;
-		    const_entry_universes = ctx;
+		    const_entry_universes =
+		      if poly then ctx else Univ.UContext.empty;
 		    const_entry_opaque = false;
 		    const_entry_inline_code = false;
 		    const_entry_feedback = None } in
 		  let k = (DefinitionEntry entry,IsDefinition kind) in
-		  let kn = declare_constant ~internal:KernelSilent fid k in
+		  let kn = declare_constant ~internal:InternalTacticRequest fid k in
 		  let constr_fip =
 		    let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
 		      applist (mkConstU (kn,u),proj_args) 
@@ -366,7 +376,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat
       mind_entry_polymorphic = poly;
       mind_entry_private = None;
       mind_entry_universes = ctx } in
-  let kn = Command.declare_mutual_inductive_with_eliminations mie [(paramimpls,[])] in
+  let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
   let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in
@@ -396,44 +406,49 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
   let impl, projs =
     match fields with
     | [(Name proj_name, _, field)] when def ->
-	let class_body = it_mkLambda_or_LetIn field params in
-        let _class_type = it_mkProd_or_LetIn arity params in
-	let class_entry = 
-	  Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in
-	let cst = Declare.declare_constant (snd id)
-	  (DefinitionEntry class_entry, IsDefinition Definition)
-	in
-	let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in
-	let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in
-	let proj_type =
-	  it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in
-	let proj_body =
-	  it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in
-	let proj_entry = Declare.definition_entry ~types:proj_type ~poly ~univs:ctx proj_body in
-	let proj_cst = Declare.declare_constant proj_name
-	  (DefinitionEntry proj_entry, IsDefinition Definition)
-	in
-	let cref = ConstRef cst in
-	Impargs.declare_manual_implicits false cref [paramimpls];
-	Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
-	Classes.set_typeclass_transparency (EvalConstRef cst) false false;
-	let sub = match List.hd coers with
-	  | Some b -> Some ((if b then Backward else Forward), List.hd priorities) 
-	  | None -> None 
-	in
-	  cref, [Name proj_name, sub, Some proj_cst]
+      let class_body = it_mkLambda_or_LetIn field params in
+      let _class_type = it_mkProd_or_LetIn arity params in
+      let class_entry = 
+	Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in
+      let cst = Declare.declare_constant (snd id)
+	(DefinitionEntry class_entry, IsDefinition Definition)
+      in
+      let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in
+      let inst_type = appvectc (mkConstU cstu)
+			       (Termops.rel_vect 0 (List.length params)) in
+      let proj_type =
+	it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in
+      let proj_body =
+	it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in
+      let proj_entry =
+	Declare.definition_entry ~types:proj_type ~poly
+	    ~univs:(if poly then ctx else Univ.UContext.empty) proj_body
+      in
+      let proj_cst = Declare.declare_constant proj_name
+        (DefinitionEntry proj_entry, IsDefinition Definition)
+      in
+      let cref = ConstRef cst in
+      Impargs.declare_manual_implicits false cref [paramimpls];
+      Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
+      Classes.set_typeclass_transparency (EvalConstRef cst) false false;
+      let sub = match List.hd coers with
+	| Some b -> Some ((if b then Backward else Forward), List.hd priorities) 
+	| None -> None 
+      in
+      cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
-	let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
+       let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
-	in
-	let coers = List.map2 (fun coe pri -> 
-			       Option.map (fun b -> 
-			         if b then Backward, pri else Forward, pri) coe) 
+       in
+       let coers = List.map2 (fun coe pri -> 
+			      Option.map (fun b -> 
+			      if b then Backward, pri else Forward, pri) coe)
 	  coers priorities
-	in
-	  IndRef ind, (List.map3 (fun (id, _, _) b y -> (id, b, y))
-			 (List.rev fields) coers (Recordops.lookup_projections ind))
+       in
+       let l = List.map3 (fun (id, _, _) b y -> (id, b, y))
+         (List.rev fields) coers (Recordops.lookup_projections ind)
+       in IndRef ind, l
   in
   let ctx_context =
     List.map (fun (na, b, t) ->
@@ -502,7 +517,7 @@ open Vernacexpr
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a
    list telling if the corresponding fields must me declared as coercions 
    or subinstances *)
-let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
+let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
   let cfs,notations = List.split cfs in
   let cfs,priorities = List.split cfs in
   let coers,fs = List.split cfs in
@@ -517,11 +532,11 @@ let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild
   if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
     error "Priorities only allowed for type class substructures";
   (* Now, younger decl in params and fields is on top *)
-  let ctx, arity, template, implpars, params, implfs, fields =
+  let (pl, ctx), arity, template, implpars, params, implfs, fields =
     States.with_state_protection (fun () ->
-      typecheck_params_and_fields (kind = Class true) idstruc s ps notations fs) () in
+      typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in
   let sign = structure_signature (fields@params) in
-    match kind with
+  let gr = match kind with
     | Class def ->
 	let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
 	  implpars params arity template implfs fields is_coe coers priorities sign in
@@ -534,3 +549,6 @@ let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild
 	  idbuild implpars params arity template implfs 
 	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
 	IndRef ind
+  in
+  Universes.register_universe_binders gr pl;
+  gr
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 91dccb96..eccb5d29 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -38,7 +38,7 @@ val declare_structure : Decl_kinds.recursivity_kind ->
   inductive
 
 val definition_structure :
-  inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * lident with_coercion * local_binder list *
+  inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * plident with_coercion * local_binder list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option -> global_reference
 
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 59283edf..9e67eef0 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -32,7 +32,7 @@ module SearchBlacklist =
       let key = ["Search";"Blacklist"]
       let title = "Current search blacklist : "
       let member_message s b =
-	str ("Search blacklist does "^(if b then "" else "not ")^"include "^s)
+	str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s
       let synchronous = true
      end)
 
@@ -253,7 +253,8 @@ let interface_search flags =
     let regexp =
       try Str.regexp s
       with e when Errors.noncritical e ->
-        Errors.error ("Invalid regexp: " ^ s)
+        Errors.errorlabstrm "Search.interface_search"
+          (str "Invalid regexp: " ++ str s)
     in
     extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
   | (Type_Pattern s, b) :: l ->
@@ -271,7 +272,8 @@ let interface_search flags =
     let id =
       try Nametab.full_name_module qid
       with Not_found ->
-        Errors.error ("Module " ^ path ^ " not found.")
+        Errors.errorlabstrm "Search.interface_search"
+          (str "Module " ++ str path ++ str " not found.")
     in
     extract_flags name tpe subtpe ((id, b) :: mods) blacklist l
   | (Include_Blacklist, b) :: l ->
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index bf0f305a..5aa7d428 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -10,6 +10,7 @@ Obligations
 Command
 Classes
 Record
+Assumptions
 Vernacinterp
 Mltop
 Vernacentries
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index f053839c..472503ce 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -42,9 +42,9 @@ let print_usage_channel co command =
 \n  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose f.)\
 \n  -lv f	                 (idem)\
 \n  -load-vernac-object f  load Coq object file f.vo\
-\n  -require f             load Coq object file f.vo and import it (Require f.)\
-\n  -compile f             compile Coq file f.v (implies -batch)\
-\n  -compile-verbose f     verbosely compile Coq file f.v (implies -batch)\
+\n  -require path          load Coq library path and import it (Require Import path.)\
+\n  -compile f.v           compile Coq file f.v (implies -batch)\
+\n  -compile-verbose f.v   verbosely compile Coq file f.v (implies -batch)\
 \n  -quick                 quickly compile .v files to .vio files (skip proofs)\
 \n  -schedule-vio2vo j f1..fn   run up to j instances of Coq to turn each fi.vio\
 \n                         into fi.vo\
@@ -52,10 +52,14 @@ let print_usage_channel co command =
 \n                         proofs in each fi.vio\
 \n\
 \n  -where                 print Coq's standard library location and exit\
-\n  -config                print Coq's configuration information and exit\
+\n  -config, --config      print Coq's configuration information and exit\
 \n  -v                     print Coq version and exit\
 \n  -list-tags             print highlight color tags known by Coq and exit\
 \n\
+\n  -quiet                 unset display of extra information (implies -w none)\
+\n  -w (all|none)          configure display of warnings\
+\n  -color (yes|no|auto)   configure color output\
+\n\
 \n  -q                     skip loading of rcfile\
 \n  -init-file f           set the rcfile to f\
 \n  -batch                 batch mode (exits just after arguments parsing)\
@@ -63,7 +67,6 @@ let print_usage_channel co command =
 \n  -bt                    print backtraces (requires configure debug flag)\
 \n  -debug                 debug mode (implies -bt)\
 \n  -emacs                 tells Coq it is executed under Emacs\
-\n  -color (on|off|auto)   configure color output (only active through coqtop)\
 \n  -noglob                do not dump globalizations\
 \n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
 \n  -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\
@@ -71,8 +74,12 @@ let print_usage_channel co command =
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
 \n  -time                  display the time taken by each command\
-\n  -no-native-compiler    disable the native_compute reduction machinery\
-\n  -h, -help              print this list of options\
+\n  -m, --memory           display total heap size at program exit\
+\n                         (use environment variable\
+\n                          OCAML_GC_STATS=\"/tmp/gclog.txt\"\
+\n                          for full Gc stats dump)
+\n  -native-compiler       precompile files for the native_compute machinery\
+\n  -h, -help, --help      print this list of options\
 \n";
   List.iter (fun (name, text) ->
     output_string co
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 176a6c33..a0cd618e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -27,7 +27,7 @@ let rec is_navigation_vernac = function
   | VernacBacktrack _
   | VernacBackTo _
   | VernacBack _ -> true
-  | VernacTime l ->
+  | VernacRedirect (_, l) | VernacTime l ->
     List.exists
       (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *)
   | c -> is_deep_navigation_vernac c
@@ -78,9 +78,13 @@ let get_exn_files e = Exninfo.get e files_of_exn
 
 let add_exn_files e f = Exninfo.add e files_of_exn f
 
-let raise_with_file f (e, info) =
-  let inner_f = match get_exn_files info with None -> f | Some ff -> ff.inner in
-  iraise (e, add_exn_files info { outer = f; inner = inner_f })
+let enrich_with_file f (e, info) =
+  let inner = match get_exn_files info with None -> f | Some x -> x.inner in
+  (e, add_exn_files info { outer = f; inner })
+
+let raise_with_file f e = iraise (enrich_with_file f e)
+
+let cur_file = ref None
 
 let disable_drop = function
   | Drop -> Errors.error "Drop is forbidden."
@@ -88,28 +92,12 @@ let disable_drop = function
 
 let user_error loc s = Errors.user_err_loc (loc,"_",str s)
 
-(* Open an utf-8 encoded file and skip the byte-order mark if any *)
-
-let open_utf8_file_in fname =
-  let is_bom s =
-    Int.equal (Char.code s.[0]) 0xEF &&
-    Int.equal (Char.code s.[1]) 0xBB &&
-    Int.equal (Char.code s.[2]) 0xBF
-  in
-  let in_chan = open_in fname in
-  let s = "   " in
-  if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
-  in_chan
-
 (* Opening and closing a channel. Open it twice when verbose: the first
    channel is used to read the commands, and the second one to print them.
    Note: we could use only one thanks to seek_in, but seeking on and on in
    the file we parse seems a bit risky to me.  B.B.  *)
 
-let open_file_twice_if verbosely fname =
-  let paths = Loadpath.get_paths () in
-  let _,longfname =
-    find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
+let open_file_twice_if verbosely longfname =
   let in_chan = open_utf8_file_in longfname in
   let verb_ch =
     if verbosely then Some (open_utf8_file_in longfname) else None in
@@ -208,26 +196,24 @@ let display_cmd_header loc com =
   let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
   in
   Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++
-	 str (" ["^cmd^"] "));
+	 str " [" ++ str cmd ++ str "] ");
   Pp.flush_all ()
 
-let rec vernac_com verbosely 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
+        let fname = CUnix.make_suffix fname ".v" in
+        let f = Loadpath.locate_file fname in
 	let st = save_translator_coqdoc () in
 	if !Flags.beautify_file then
 	  begin
-            let paths = Loadpath.get_paths () in
-            let _,f = find_file_in_path ~warn:(Flags.is_verbose())
-	      paths
-	      (CUnix.make_suffix fname ".v") in
 	    chan_beautify := open_out (f^beautify_suffix);
 	    Pp.comments := []
           end;
 	begin
 	  try
-            read_vernac_file verbosely (CUnix.make_suffix fname ".v");
+            read_vernac_file verbosely f;
 	    restore_translator_coqdoc st;
 	  with reraise ->
             let reraise = Errors.push reraise in
@@ -237,7 +223,7 @@ let rec vernac_com verbosely checknav (loc,com) =
 
     | v when !just_parsing -> ()
 
-    | v -> Stm.interp verbosely (loc,v)
+    | v -> Stm.interp verbose (loc,v)
   in
     try
       checknav loc com;
@@ -253,13 +239,12 @@ let rec vernac_com verbosely checknav (loc,com) =
       else iraise (reraise, info)
 
 and read_vernac_file verbosely s =
-  Flags.make_warn verbosely;
   let checknav loc cmd =
     if is_navigation_vernac cmd && not (is_reset cmd) then
 	user_error loc "Navigation commands forbidden in files"
   in
-  let (in_chan, fname, input) =
-    open_file_twice_if verbosely s in
+  let (in_chan, fname, input) = open_file_twice_if verbosely s in
+  cur_file := Some fname;
   try
     (* we go out of the following infinite loop when a End_of_input is
      * raised, which means that we raised the end of the file being loaded *)
@@ -274,6 +259,7 @@ and read_vernac_file verbosely s =
     close_input in_chan input;    (* we must close the file first *)
     match e with
       | End_of_input ->
+          cur_file := None;
           if do_beautify () then
             pr_new_syntax (Loc.make_loc (max_int,max_int)) None
       | _ -> raise_with_file fname (disable_drop e, info)
@@ -296,14 +282,22 @@ let load_vernac verb file =
   chan_beautify :=
     if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
   try
-    read_vernac_file verb file;
+    Flags.silently (read_vernac_file verb) file;
     if !Flags.beautify_file then close_out !chan_beautify;
   with any ->
     let (e, info) = Errors.push any in
     if !Flags.beautify_file then close_out !chan_beautify;
     raise_with_file file (disable_drop e, info)
 
-(* Compile a vernac file (f is assumed without .v suffix) *)
+let ensure_v f =
+  if Filename.check_suffix f ".v" then f
+  else begin
+    msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
+    expanded to \"" ++ str f ++ str ".v\"");
+    f ^ ".v"
+  end
+
+(* Compile a vernac file *)
 let compile verbosely f =
   let check_pending_proofs () =
     let pfs = Pfedit.get_all_proof_names () in
@@ -311,7 +305,8 @@ let compile verbosely f =
       (msg_error (str "There are pending proofs"); flush_all (); exit 1) in
   match !Flags.compilation_mode with
   | BuildVo ->
-      let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
+      let long_f_dot_v = ensure_v f in
+      let ldir = Flags.verbosely Library.start_library long_f_dot_v in
       Stm.set_compilation_hints long_f_dot_v;
       Aux_file.start_aux_file_for long_f_dot_v;
       Dumpglob.start_dump_glob long_f_dot_v;
@@ -327,7 +322,8 @@ let compile verbosely f =
       Aux_file.stop_aux_file ();
       Dumpglob.end_dump_glob ()
   | BuildVio ->
-      let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in
+      let long_f_dot_v = ensure_v f in
+      let ldir = Flags.verbosely Library.start_library long_f_dot_v in
       Dumpglob.noglob ();
       Stm.set_compilation_hints long_f_dot_v;
       let _ = load_vernac verbosely long_f_dot_v in
@@ -340,13 +336,18 @@ let compile verbosely f =
       let open Library in
       Dumpglob.noglob ();
       let f = if check_suffix f ".vio" then chop_extension f else f in
-      let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
+      let lfdv, sum, lib, univs, disch, tasks, proofs = load_library_todo f in
       Stm.set_compilation_hints lfdv;
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
-      Library.save_library_raw lfdv lib univs proofs
+      Library.save_library_raw lfdv sum lib univs proofs
 
 let compile v f = 
   ignore(CoqworkmgrApi.get 1);
   compile v f;
   CoqworkmgrApi.giveback 1
 
+let () = Hook.set Stm.process_error_hook (fun e ->
+  match !cur_file with
+  | None -> Cerrors.process_vernac_interp_error e
+  | Some f -> enrich_with_file f (Cerrors.process_vernac_interp_error e)
+)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index cfa9bddc..b6a1a53f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -76,9 +76,8 @@ let show_universes () =
   let gls = Proof.V82.subgoals pfts in
   let sigma = gls.Evd.sigma in
   let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
-  let cstrs = Univ.merge_constraints (Univ.ContextSet.constraints ctx) Univ.empty_universes in
     msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma));
-    msg_notice (str"Normalized constraints: " ++ Univ.pr_universes (Evd.pr_evd_level sigma) cstrs)
+    msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx)
 
 let show_prooftree () =
   (* Spiwack: proof tree is currently not working *)
@@ -102,17 +101,16 @@ let try_print_subgoals () =
 let show_intro all =
   let pf = get_pftreestate() in
   let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
-  let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
-  let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
-  if all
-  then
-    let lid = Tactics.find_intro_names l gl in
-    msg_notice (hov 0 (prlist_with_sep  spc pr_id lid))
-  else
-    try
+  if not (List.is_empty gls) then begin
+    let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
+    let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
+    if all then
+      let lid = Tactics.find_intro_names l gl in
+      msg_notice (hov 0 (prlist_with_sep  spc pr_id lid))
+    else if not (List.is_empty l) then
       let n = List.last l in
       msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
-    with Failure "List.last" -> ()
+  end
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
@@ -351,7 +349,7 @@ let dump_universes_gen g s =
   try
     Univ.dump_universes output_constraint g;
     close ();
-    msg_info (str ("Universes written to file \""^s^"\"."))
+    msg_info (str "Universes written to file \"" ++ str s ++ str "\".")
   with reraise ->
     let reraise = Errors.push reraise in
     close ();
@@ -366,8 +364,7 @@ let dump_universes sorted s =
 (* "Locate" commands *)
 
 let locate_file f =
-  let paths = Loadpath.get_paths () in
-  let _, file = System.find_file_in_path ~warn:false paths f in
+  let file = Flags.silently Loadpath.locate_file f in
   str file
 
 let msg_found_library = function
@@ -379,17 +376,27 @@ let msg_found_library = function
       msg_info (hov 0
 	(pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file))
 
-let err_unmapped_library loc qid =
+let err_unmapped_library loc ?from qid =
   let dir = fst (repr_qualid qid) in
+  let prefix = match from with
+  | None -> str "."
+  | Some from ->
+    str " and prefix " ++ pr_dirpath from ++ str "."
+  in
   user_err_loc
     (loc,"locate_library",
-     strbrk "Cannot find a physical path bound to logical path " ++
-       pr_dirpath dir ++ str".")
+     strbrk "Cannot find a physical path bound to logical path matching suffix " ++
+       pr_dirpath dir ++ prefix)
 
-let err_notfound_library loc qid =
+let err_notfound_library loc ?from qid =
+  let prefix = match from with
+  | None -> str "."
+  | Some from ->
+    str " with prefix " ++ pr_dirpath from ++ str "."
+  in
   user_err_loc
     (loc,"locate_library",
-     strbrk "Unable to locate library " ++ pr_qualid qid ++ str".")
+     strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
 
 let print_located_library r =
   let (loc,qid) = qualid_of_reference r in
@@ -415,7 +422,9 @@ let vernac_syntax_extension locality local =
   let local = enforce_module_locality locality local in
   Metasyntax.add_syntax_extension local
 
-let vernac_delimiters = Metasyntax.add_delimiters
+let vernac_delimiters sc = function
+  | Some lr -> Metasyntax.add_delimiters sc lr
+  | None -> Metasyntax.remove_delimiters sc
 
 let vernac_bind_scope sc cll =
   Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll)
@@ -450,7 +459,7 @@ let vernac_definition_hook p = function
 | SubClass -> Class.add_subclass_hook p
 | _ -> no_hook
 
-let vernac_definition locality p (local,k) (loc,id as lid) def =
+let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
   let local = enforce_locality_exp locality local in
   let hook = vernac_definition_hook p k in
   let () = match local with
@@ -460,26 +469,27 @@ let vernac_definition locality p (local,k) (loc,id as lid) def =
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
  	  start_proof_and_print (local,p,DefinitionBody Definition)
-	    [Some lid, (bl,t,None)] no_hook
+	    [Some (lid,pl), (bl,t,None)] no_hook
     | DefineBody (bl,red_option,c,typ_opt) ->
  	let red_option = match red_option with
           | None -> None
           | Some r ->
 	      let (evc,env)= get_current_context () in
  		Some (snd (interp_redexp env evc r)) in
-	do_definition id (local,p,k) bl red_option c typ_opt hook)
+	do_definition id (local,p,k) pl bl red_option c typ_opt hook)
 
-let vernac_start_proof p kind l lettop =
+let vernac_start_proof locality p kind l lettop =
+  let local = enforce_locality_exp locality None in
   if Dumpglob.dump () then
     List.iter (fun (id, _) ->
       match id with
-	| Some lid -> Dumpglob.dump_definition lid false "prf"
+	| Some (lid,_) -> Dumpglob.dump_definition lid false "prf"
 	| None -> ()) l;
   if not(refining ()) then
     if lettop then
       errorlabstrm "Vernacentries.StartProof"
 	(str "Let declarations can only be used in proof editing mode.");
-  start_proof_and_print (Global, p, Proof kind) l no_hook
+  start_proof_and_print (local, p, Proof kind) l no_hook
 
 let qed_display_script = ref true
 
@@ -506,7 +516,7 @@ let vernac_assumption locality poly (local, kind) l nl =
   let kind = local, poly, kind in
   List.iter (fun (is_coe,(idl,c)) ->
     if Dumpglob.dump () then
-      List.iter (fun lid ->
+      List.iter (fun (lid, _) ->
 	if global then Dumpglob.dump_definition lid false "ax"
 	else Dumpglob.dump_definition lid true "var") idl) l;
   let status = do_assumptions kind nl l in
@@ -514,11 +524,11 @@ let vernac_assumption locality poly (local, kind) l nl =
 
 let vernac_record k poly finite struc binders sort nameopt cfs =
   let const = match nameopt with
-    | None -> add_prefix "Build_" (snd (snd struc))
+    | None -> add_prefix "Build_" (snd (fst (snd struc)))
     | Some (_,id as lid) ->
 	Dumpglob.dump_definition lid false "constr"; id in
     if Dumpglob.dump () then (
-      Dumpglob.dump_definition (snd struc) false "rec";
+      Dumpglob.dump_definition (fst (snd struc)) false "rec";
       List.iter (fun (((_, x), _), _) ->
 	match x with
 	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
@@ -527,7 +537,7 @@ let vernac_record k poly finite struc binders sort nameopt cfs =
 
 let vernac_inductive poly lo finite indl =
   if Dumpglob.dump () then
-    List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
+    List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
       match cstrs with
 	| Constructors cstrs ->
 	    Dumpglob.dump_definition lid false "ind";
@@ -542,12 +552,12 @@ let vernac_inductive poly lo finite indl =
       Errors.error "The Variant keyword cannot be used to define a record type. Use Record instead."
   | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
       vernac_record (match b with Class true -> Class false | _ -> b)
-	poly finite id bl c oc fs
+       poly finite id bl c oc fs
   | [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
       let f =
 	let (coe, ((loc, id), ce)) = l in
 	let coe' = if coe then Some true else None in
-	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
+  	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
       in vernac_record (Class true) poly finite id bl c None [f]
   | [ ( id , bl , c , Class true, _), _ ] ->
       Errors.error "Definitional classes must have a single method"
@@ -567,13 +577,13 @@ let vernac_inductive poly lo finite indl =
 let vernac_fixpoint locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
-    List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
+    List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   do_fixpoint local poly l
 
 let vernac_cofixpoint locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
-    List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
+    List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   do_cofixpoint local poly l
 
 let vernac_scheme l =
@@ -592,8 +602,19 @@ let vernac_combined_scheme lid l =
      List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l);
  Indschemes.do_combined_scheme lid l
 
-let vernac_universe l = do_universe l
-let vernac_constraint l = do_constraint l
+let vernac_universe loc poly l =
+  if poly && not (Lib.sections_are_opened ()) then
+    user_err_loc (loc, "vernac_universe",
+		  str"Polymorphic universes can only be declared inside sections, " ++
+		  str "use Monomorphic Universe instead");
+  do_universe poly l
+
+let vernac_constraint loc poly l =
+  if poly && not (Lib.sections_are_opened ()) then
+    user_err_loc (loc, "vernac_constraint",
+		  str"Polymorphic universe constraints can only be declared"
+		  ++ str " inside sections, use Monomorphic Constraint instead");
+  do_constraint poly l
 
 (**********************)
 (* Modules            *)
@@ -610,16 +631,14 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
   let binders_ast = List.map
    (fun (export,idl,ty) ->
      if not (Option.is_empty export) then
-      error ("Arguments of a functor declaration cannot be exported. " ^
-       "Remove the \"Export\" and \"Import\" keywords from every functor " ^
-       "argument.")
+      error "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument."
      else (idl,ty)) binders_ast in
   let mp =
     Declaremods.declare_module Modintern.interp_module_ast
       id binders_ast (Enforce mty_ast) []
   in
   Dumpglob.dump_moddef loc mp "mod";
-  if_verbose msg_info (str ("Module "^ Id.to_string id ^" is declared"));
+  if_verbose msg_info (str "Module " ++ pr_id id ++ str " is declared");
   Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
 
 let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
@@ -641,7 +660,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        in
        Dumpglob.dump_moddef loc mp "mod";
        if_verbose msg_info
-         (str ("Interactive Module "^ Id.to_string id ^" started"));
+         (str "Interactive Module " ++ pr_id id ++ str " started");
        List.iter
          (fun (export,id) ->
            Option.iter
@@ -651,9 +670,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        let binders_ast = List.map
         (fun (export,idl,ty) ->
           if not (Option.is_empty export) then
-           error ("Arguments of a functor definition can be imported only if" ^
-                  " the definition is interactive. Remove the \"Export\" and " ^
-                  "\"Import\" keywords from every functor argument.")
+           error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument."
           else (idl,ty)) binders_ast in
        let mp =
          Declaremods.declare_module Modintern.interp_module_ast
@@ -661,14 +678,14 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        in
        Dumpglob.dump_moddef loc mp "mod";
        if_verbose msg_info
-	 (str ("Module "^ Id.to_string id ^" is defined"));
+	 (str "Module " ++ pr_id id ++ str " is defined");
        Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)])
          export
 
 let vernac_end_module export (loc,id as lid) =
   let mp = Declaremods.end_module () in
   Dumpglob.dump_modref loc mp "mod";
-  if_verbose msg_info (str ("Module "^ Id.to_string id ^" is defined"));
+  if_verbose msg_info (str "Module " ++ pr_id id ++ str " is defined");
   Option.iter (fun export -> vernac_import export [Ident lid]) export
 
 let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
@@ -690,7 +707,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
        in
        Dumpglob.dump_moddef loc mp "modtype";
        if_verbose msg_info
-	 (str ("Interactive Module Type "^ Id.to_string id ^" started"));
+	 (str "Interactive Module Type " ++ pr_id id ++ str " started");
        List.iter
          (fun (export,id) ->
            Option.iter
@@ -701,9 +718,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
 	let binders_ast = List.map
           (fun (export,idl,ty) ->
             if not (Option.is_empty export) then
-              error ("Arguments of a functor definition can be imported only if" ^
-			" the definition is interactive. Remove the \"Export\" " ^
-			"and \"Import\" keywords from every functor argument.")
+              error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument."
             else (idl,ty)) binders_ast in
 	let mp =
           Declaremods.declare_modtype Modintern.interp_module_ast
@@ -711,12 +726,12 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
         in
         Dumpglob.dump_moddef loc mp "modtype";
 	if_verbose msg_info
-	  (str ("Module Type "^ Id.to_string id ^" is defined"))
+	  (str "Module Type " ++ pr_id id ++ str " is defined")
 
 let vernac_end_modtype (loc,id) =
   let mp = Declaremods.end_modtype () in
   Dumpglob.dump_modref loc mp "modtype";
-  if_verbose msg_info (str ("Module Type "^ Id.to_string id ^" is defined"))
+  if_verbose msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
 
 let vernac_include l =
   Declaremods.declare_include Modintern.interp_module_ast l
@@ -765,8 +780,8 @@ let vernac_require from import qidl =
       let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in
       (dir, f)
     with
-      | Library.LibUnmappedDir -> err_unmapped_library loc qid
-      | Library.LibNotFound -> err_notfound_library loc qid
+      | Library.LibUnmappedDir -> err_unmapped_library loc ?from:root qid
+      | Library.LibNotFound -> err_notfound_library loc ?from:root qid
   in
   let modrefl = List.map locate qidl in
   if Dumpglob.dump () then
@@ -868,20 +883,10 @@ let vernac_set_used_variables e =
   let vars = Environ.named_context env in
   List.iter (fun id -> 
     if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then
-      error ("Unknown variable: " ^ Id.to_string id))
+      errorlabstrm "vernac_set_used_variables"
+        (str "Unknown variable: " ++ pr_id id))
     l;
-  let closure_l = List.map pi1 (set_used_variables l) in
-  let closure_l = List.fold_right Id.Set.add closure_l Id.Set.empty in
-  let vars_of = Environ.global_vars_set in
-  let aux env entry (all_safe,rest as orig) =
-    match entry with
-    | (x,None,_) ->
-       if Id.Set.mem x all_safe then orig else (all_safe, (Loc.ghost,x)::rest) 
-    | (x,Some bo, ty) ->
-       let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
-       if Id.Set.subset vars all_safe then (Id.Set.add x all_safe, rest)
-       else (all_safe, (Loc.ghost,x) :: rest) in
-  let _,to_clear = Environ.fold_named_context aux env ~init:(closure_l,[]) in
+  let _, to_clear = set_used_variables l in
   vernac_solve
     SelectAll None Tacexpr.(TacAtom (Loc.ghost,TacClear(false,to_clear))) false
 
@@ -914,7 +919,7 @@ let vernac_chdir = function
   | Some path ->
       begin
 	try Sys.chdir (expand path)
-	with Sys_error err -> msg_warning (str ("Cd failed: " ^ err))
+	with Sys_error err -> msg_warning (str "Cd failed: " ++ str err)
       end;
       if_verbose msg_info (str (Sys.getcwd()))
 
@@ -924,10 +929,12 @@ let vernac_chdir = function
 
 let vernac_write_state file =
   Pfedit.delete_all_proofs ();
+  let file = CUnix.make_suffix file ".coq" in
   States.extern_state file
 
 let vernac_restore_state file =
   Pfedit.delete_all_proofs ();
+  let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in
   States.intern_state file
 
 (************)
@@ -1051,15 +1058,16 @@ let vernac_declare_arguments locality r l nargs flags =
   let inf_names =
     let ty = Global.type_of_global_unsafe sr in
       Impargs.compute_implicits_names (Global.env ()) ty in
-  let string_of_name = function Anonymous -> "_" | Name id -> Id.to_string id in
   let rec check li ld ls = match li, ld, ls with
     | [], [], [] -> ()
     | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls
     | [], _::_, (Some _)::ls when extra_scope_flag ->
        error "Extra notation scopes can be set on anonymous arguments only"
-    | [], x::_, _ -> error ("Extra argument " ^ string_of_name x ^ ".")
-    | l, [], _ -> error ("The following arguments are not declared: " ^
-       (String.concat ", " (List.map string_of_name l)) ^ ".")
+    | [], x::_, _ -> errorlabstrm "vernac_declare_arguments"
+                       (str "Extra argument " ++ pr_name x ++ str ".")
+    | l, [], _ -> errorlabstrm "vernac_declare_arguments"
+                    (str "The following arguments are not declared: " ++
+                       prlist_with_sep pr_comma pr_name l ++ str ".")
     | _::li, _::ld, _::ls -> check li ld ls 
     | _ -> assert false in
   let () = match l with
@@ -1087,9 +1095,6 @@ let vernac_declare_arguments locality r l nargs flags =
   let renamed_arg = ref None in
   let set_renamed a b =
     if Option.is_empty !renamed_arg && not (Id.equal a b) then renamed_arg := Some(b,a) in
-  let pr_renamed_arg () = match !renamed_arg with None -> ""
-    | Some (o,n) ->
-       "\nArgument "^string_of_id o ^" renamed to "^string_of_id n^"." in
   let some_renaming_specified =
     try
       let names = Arguments_renaming.arguments_names sr in
@@ -1103,7 +1108,8 @@ let vernac_declare_arguments locality r l nargs flags =
       let sr', impl = List.fold_map (fun b -> function
         | (Anonymous, _,_, true, max), Name id -> assert false
         | (Name x, _,_, true, _), Anonymous ->
-            error ("Argument "^Id.to_string x^" cannot be declared implicit.")
+            errorlabstrm "vernac_declare_arguments"
+              (str "Argument " ++ pr_id x ++ str " cannot be declared implicit.")
         | (Name iid, _,_, true, max), Name id ->
            set_renamed iid id;
            b || not (Id.equal iid id), Some (ExplByName id, max, false)
@@ -1116,8 +1122,12 @@ let vernac_declare_arguments locality r l nargs flags =
       some_renaming_specified l in
   if some_renaming_specified then
     if not (List.mem `Rename flags) then
-      error ("To rename arguments the \"rename\" flag must be specified."
-        ^ pr_renamed_arg ())
+      errorlabstrm "vernac_declare_arguments"
+        (str "To rename arguments the \"rename\" flag must be specified." ++
+           match !renamed_arg with
+           | None -> mt ()
+           | Some (o,n) ->
+              str "\nArgument " ++ pr_id o ++ str " renamed to " ++ pr_id n ++ str ".")
     else
       Arguments_renaming.rename_arguments
         (make_section_locality locality) sr names_decl;
@@ -1175,8 +1185,9 @@ let default_env () = {
 let vernac_reserve bl =
   let sb_decl = (fun (idl,c) ->
     let env = Global.env() in
-    let t,ctx = Constrintern.interp_type env Evd.empty c in
-    let t = Detyping.detype false [] env Evd.empty t in
+    let sigma = Evd.from_env env in
+    let t,ctx = Constrintern.interp_type env sigma c in
+    let t = Detyping.detype false [] env (Evd.from_ctx ctx) t in
     let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl
@@ -1348,19 +1359,10 @@ let _ =
       optwrite = Flags.make_universe_polymorphism }
 
 let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "use of virtual machine inside the kernel";
-      optkey   = ["Virtual";"Machine"];
-      optread  = (fun () -> Vconv.use_vm ());
-      optwrite = (fun b -> Vconv.set_use_vm b) }
-
-let _ =
   declare_int_option
     { optsync  = true;
       optdepr  = false;
-      optname  = "the level of inling duging functor application";
+      optname  = "the level of inlining during functor application";
       optkey   = ["Inline";"Level"];
       optread  = (fun () -> Some (Flags.get_inline_level ()));
       optwrite = (fun o ->
@@ -1376,15 +1378,6 @@ let _ =
       optread  = (fun () -> !Closure.share);
       optwrite = (fun b -> Closure.share := b) }
 
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "use of boxed values";
-      optkey   = ["Boxed";"Values"];
-      optread  = (fun _ -> not (Vm.transp_values ()));
-      optwrite = (fun b -> Vm.set_transp_values (not b)) }
-
 (* No more undo limit in the new proof engine.
    The command still exists for compatibility (e.g. with ProofGeneral) *)
 
@@ -1432,6 +1425,15 @@ let _ =
       optkey   = ["Printing";"Universes"];
       optread  = (fun () -> !Constrextern.print_universes);
       optwrite = (fun b -> Constrextern.print_universes:=b) }
+     
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "dumping bytecode after compilation";
+      optkey   = ["Dump";"Bytecode"];
+      optread  = Flags.get_dump_bytecode;
+      optwrite = Flags.set_dump_bytecode }
 
 let vernac_debug b =
   set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
@@ -1478,6 +1480,8 @@ let vernac_set_opacity locality (v,l) =
 
 let vernac_set_option locality key = function
   | StringValue s -> set_string_option_value_gen locality key s
+  | StringOptValue (Some s) -> set_string_option_value_gen locality key s
+  | StringOptValue None -> unset_option_value_gen locality key
   | IntValue n -> set_int_option_value_gen locality key n
   | BoolValue b -> set_bool_option_value_gen locality key b
 
@@ -1523,7 +1527,7 @@ let vernac_check_may_eval redexp glopt rc =
   let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in
   Evarconv.check_problems_are_solved env sigma';
   let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
-  let uctx = Evd.universe_context sigma' in
+  let pl, uctx = Evd.universe_context sigma' in
   let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in
   let c = nf c in
   let j =
@@ -1538,7 +1542,7 @@ let vernac_check_may_eval redexp glopt rc =
         let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
 	msg_notice (print_judgment env sigma' j ++
                     pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
-                    Printer.pr_universe_ctx uctx)
+                    Printer.pr_universe_ctx sigma uctx)
     | Some r ->
         Tacintern.dump_glob_red_expr r;
         let (sigma',r_interp) = interp_redexp env sigma' r in
@@ -1555,7 +1559,7 @@ let vernac_global_check c =
   let sigma = Evd.from_env env in
   let c,ctx = interp_constr env sigma c in
   let senv = Global.safe_env() in
-  let cstrs = snd (Evd.evar_universe_context_set ctx) in
+  let cstrs = snd (Evd.evar_universe_context_set Univ.UContext.empty ctx) in
   let senv = Safe_typing.add_constraints cstrs senv in
   let j = Safe_typing.typing senv c in
   let env = Safe_typing.env_of_safe_env senv in
@@ -1581,7 +1585,8 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
       | Some n,AN (Ident (_loc,id)) ->  (* goal number given, catch if wong *)
 	 (try get_nth_goal n,id
 	  with
-	    Failure _ -> Errors.error ("No such goal: "^string_of_int n^"."))
+	    Failure _ -> errorlabstrm "print_about_hyp_globs"
+                           (str "No such goal: " ++ int n ++ str "."))
       | _ , _ -> raise NoHyp in
     let hyps = pf_hyps gl in
     let (id,bdyopt,typ) = Context.lookup_named id hyps in
@@ -1619,9 +1624,13 @@ let vernac_print = function
       msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
   | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ())
   | PrintUniverses (b, None) ->
-    let univ = Global.universes () in
-    let univ = if b then Univ.sort_universes univ else univ in
-    msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ)
+     let univ = Global.universes () in
+     let univ = if b then Univ.sort_universes univ else univ in
+     let pr_remaining =
+       if Global.is_joined_environment () then mt ()
+       else str"There may remain asynchronous universe constraints"
+     in
+     msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
   | PrintUniverses (b, Some s) -> dump_universes b s
   | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
   | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())
@@ -1640,10 +1649,11 @@ let vernac_print = function
     dump_global qid; msg_notice (print_impargs qid)
   | PrintAssumptions (o,t,r) ->
       (* Prints all the axioms and section variables used by a term *)
-      let cstr = printable_constr_of_global (smart_global r) in
+      let gr = smart_global r in
+      let cstr = printable_constr_of_global gr in
       let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in
       let nassums =
-	Assumptions.assumptions st ~add_opaque:o ~add_transparent:t cstr in
+	Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in
       msg_notice (Printer.pr_assumptionset (Global.env ()) nassums)
   | PrintStrategy r -> print_strategy r
 
@@ -1674,8 +1684,8 @@ let interp_search_about_item env =
 	    (fun _ -> true) s sc in
 	GlobSearchSubPattern (Pattern.PRef ref)
       with UserError _ ->
-	error ("Unable to interp \""^s^"\" either as a reference or \
-          	as an identifier component")
+	errorlabstrm "interp_search_about_item"
+          (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")
 
 let vernac_search s gopt r =
   let r = interp_search_restriction r in
@@ -1776,6 +1786,7 @@ let vernac_show = function
       | OpenSubgoals -> pr_open_subgoals ()
       | NthGoal n -> pr_nth_open_subgoal n
       | GoalId id -> pr_goal_by_id id
+      | GoalUid id -> pr_goal_by_uid id
     in
     msg_notice info
   | ShowGoalImplicitly None ->
@@ -1817,23 +1828,11 @@ let vernac_load interp fname =
     match Pcoq.Gram.entry_parse Pcoq.main_entry po with
       | Some x -> x
       | None -> raise End_of_input) in
-  let open_utf8_file_in fname =
-    let is_bom s =
-      Int.equal (Char.code s.[0]) 0xEF &&
-      Int.equal (Char.code s.[1]) 0xBB &&
-      Int.equal (Char.code s.[2]) 0xBF
-    in
-    let in_chan = open_in fname in
-    let s = "   " in
-    if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
-    in_chan in
   let fname =
     Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
   let fname = CUnix.make_suffix fname ".v" in
   let input =
-    let paths = Loadpath.get_paths () in
-    let _,longfname =
-      System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
+    let longfname = Loadpath.locate_file fname in
     let in_chan = open_utf8_file_in longfname in
     Pcoq.Gram.parsable (Stream.of_channel in_chan) in
   try while true do interp (snd (parse_sentence input)) done
@@ -1842,14 +1841,16 @@ let vernac_load interp fname =
 
 (* "locality" is the prefix "Local" attribute, while the "local" component
  * is the outdated/deprecated "Local" attribute of some vernacular commands
- * still parsed as the obsolete_locality grammar entry for retrocompatibility *)
-let interp ?proof locality poly c =
+ * still parsed as the obsolete_locality grammar entry for retrocompatibility.
+ * loc is the Loc.t of the vernacular command being interpreted. *)
+let interp ?proof ~loc locality poly c =
   prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
   match c with
   (* Done later in this file *)
   | VernacLoad _ -> assert false
   | VernacFail _ -> assert false
   | VernacTime _ -> assert false
+  | VernacRedirect _ -> assert false
   | VernacTimeout _ -> assert false
   | VernacStm _ -> assert false
 
@@ -1872,7 +1873,7 @@ let interp ?proof locality poly c =
 
   (* Gallina *)
   | VernacDefinition (k,lid,d) -> vernac_definition locality poly k lid d
-  | VernacStartTheoremProof (k,l,top) -> vernac_start_proof poly k l top
+  | VernacStartTheoremProof (k,l,top) -> vernac_start_proof locality poly k l top
   | VernacEndProof e -> vernac_end_proof ?proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
@@ -1881,8 +1882,8 @@ let interp ?proof locality poly c =
   | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
-  | VernacUniverse l -> vernac_universe l
-  | VernacConstraint l -> vernac_constraint l
+  | VernacUniverse l -> vernac_universe loc poly l
+  | VernacConstraint l -> vernac_constraint loc poly l
 
   (* Modules *)
   | VernacDeclareModule (export,lid,bl,mtyo) ->
@@ -1977,7 +1978,7 @@ let interp ?proof locality poly c =
   | VernacBacktrack _ -> msg_warning (str "VernacBacktrack not handled by Stm")
   
   (* Proof management *)
-  | VernacGoal t -> vernac_start_proof poly Theorem [None,([],t,None)] false
+  | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
   | VernacUnfocused -> vernac_unfocused ()
@@ -1986,10 +1987,16 @@ let interp ?proof locality poly c =
   | VernacEndSubproof -> vernac_end_subproof ()
   | VernacShow s -> vernac_show s
   | VernacCheckGuard -> vernac_check_guard ()
-  | VernacProof (None, None) -> ()
-  | VernacProof (Some tac, None) -> vernac_set_end_tac tac
-  | VernacProof (None, Some l) -> vernac_set_used_variables l
+  | VernacProof (None, None) ->
+      Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:no"
+  | VernacProof (Some tac, None) ->
+      Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:no";
+      vernac_set_end_tac tac
+  | VernacProof (None, Some l) ->
+      Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:yes";
+      vernac_set_used_variables l
   | VernacProof (Some tac, Some l) -> 
+      Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:yes";
       vernac_set_end_tac tac; vernac_set_used_variables l
   | VernacProofMode mn -> Proof_global.set_proof_mode mn
   (* Toplevel control *)
@@ -2012,7 +2019,7 @@ let check_vernac_supports_locality c l =
     | VernacOpenCloseScope _
     | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
     | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
-    | VernacAssumption _
+    | VernacAssumption _ | VernacStartTheoremProof _
     | VernacCoercion _ | VernacIdentityCoercion _
     | VernacInstance _ | VernacDeclareInstances _
     | VernacDeclareMLModule _
@@ -2039,7 +2046,7 @@ let check_vernac_supports_polymorphism c p =
     | VernacCoercion _ | VernacIdentityCoercion _
     | VernacInstance _ | VernacDeclareInstances _
     | VernacHints _ | VernacContext _
-    | VernacExtend _ ) -> ()
+    | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> ()
   | Some _, _ -> Errors.error "This command does not support Polymorphism"
 
 let enforce_polymorphism = function
@@ -2096,7 +2103,7 @@ let with_fail b f =
            | e ->
               let e = Errors.push e in
               raise (HasFailed (Errors.iprint
-                (Cerrors.process_vernac_interp_error ~with_header:false e))))
+                (Cerrors.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e))))
         ()
     with e when Errors.noncritical e -> 
       let (e, _) = Errors.push e in
@@ -2104,7 +2111,7 @@ let with_fail b f =
       | HasNotFailed ->
           errorlabstrm "Fail" (str "The command has not failed!")
       | HasFailed msg ->
-          if is_verbose () || !Flags.ide_slave then msg_info
+          if is_verbose () || !test_mode || !ide_slave then msg_info
             (str "The command has indeed failed with message:" ++ fnl () ++ msg)
       | _ -> assert false
   end
@@ -2128,6 +2135,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
     | VernacTimeout (n,v) ->
         current_timeout := Some n;
         aux ?locality ?polymorphism isprogcmd v
+    | VernacRedirect (s, v) ->
+         Pp.with_output_to_file s (aux_list ?locality ?polymorphism isprogcmd) v;
     | VernacTime v ->
         System.with_time !Flags.time
           (aux_list ?locality ?polymorphism isprogcmd) v;
@@ -2139,8 +2148,9 @@ let interp ?(verbosely=true) ?proof (loc,c) =
         Obligations.set_program_mode isprogcmd;
         try
           vernac_timeout begin fun () ->
-          if verbosely then Flags.verbosely (interp ?proof locality poly) c
-                       else Flags.silently  (interp ?proof locality poly) c;
+          if verbosely
+            then Flags.verbosely (interp ?proof ~loc locality poly) c
+            else Flags.silently  (interp ?proof ~loc locality poly) c;
           if orig_program_mode || not !Flags.program_mode || isprogcmd then
             Flags.program_mode := orig_program_mode
           end
@@ -2162,5 +2172,4 @@ let interp ?(verbosely=true) ?proof (loc,c) =
     else aux false c
 
 let () = Hook.set Stm.interp_hook interp
-let () = Hook.set Stm.process_error_hook Cerrors.process_vernac_interp_error
 let () = Hook.set Stm.with_fail_hook with_fail
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 4b1cd7a0..c6d87596 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -16,6 +16,9 @@ val show_prooftree : unit -> unit
 
 val show_node : unit -> unit
 
+val vernac_require :
+  Libnames.reference option -> bool option -> Libnames.reference list -> unit
+
 (** This function can be used by any command that want to observe terms
    in the context of the current goal *)
 val get_current_context_of_args : int option -> Evd.evar_map * Environ.env