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

47 files changed, 1222 insertions, 1422 deletions

diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index a11653a43b..1802b2d366 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -23,6 +23,7 @@ open Declarations
 open Mod_subst
 open Globnames
 open Printer
+open Context.Named.Declaration
 
 (** 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]
@@ -55,7 +56,7 @@ let rec fields_of_functor f subs mp0 args = function
     match args with
     | [] -> assert false (* we should only encounter applied functors *)
     | mpa :: args ->
-      let subs = add_mbid mbid mpa empty_delta_resolver (*TODO*) subs in
+      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 =
@@ -64,11 +65,11 @@ let rec lookup_module_in_impl mp =
     (* 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 _ | MPbound _ ->
-	raise Not_found (* should have been found by [lookup_module] *)
-      | MPdot (mp',lab') ->
-	let fields = memoize_fields_of_mp mp' in
-	search_mod_label lab' fields
+    | 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
@@ -141,58 +142,131 @@ let label_of = function
   | 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
+  let body () = Global.lookup_named id |> get_value 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)
+| Ind ((mind, _) as ind, _) ->
+  traverse_inductive accu mind (IndRef ind)
+| Construct (((mind, _), _) as cst, _) ->
+  traverse_inductive accu mind (ConstructRef cst)
 | Meta _ | Evar _ -> assert false
 | Case (_,oty,c,[||]) ->
-    (* non dependent match on an inductive with no constructors *) 
+    (* non dependent match on an inductive with no constructors *)
     begin match Constr.(kind oty, kind c) with
-    | Lambda(Anonymous,_,oty), Const (kn, _)
+    | Lambda(_,_,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
+        Termops.fold_constr_with_full_binders
+          Context.Rel.add (traverse current) ctx accu t
     end
-| _ -> Termops.fold_constr_with_full_binders push (traverse current) ctx accu t
+| _ -> Termops.fold_constr_with_full_binders
+          Context.Rel.add (traverse current) ctx accu t
 
 and traverse_object ?inhabits (curr, data, ax2ty) body obj =
   let data, ax2ty =
-    let already_in = Refmap.mem obj data in
+    let already_in = Refmap_env.mem obj data in
     match body () with
     | None ->
         let data =
-          if not already_in then Refmap.add obj Refset.empty data else data in
+          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.find obj ax2ty in Refmap.add obj (ty::l) ax2ty 
-          with Not_found -> Refmap.add obj [ty] ax2ty 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.empty,data,ax2ty) body in
-      Refmap.add obj contents data, ax2ty
+        traverse (label_of obj) Context.Rel.empty
+                 (Refset_env.empty,data,ax2ty) body in
+      Refmap_env.add obj contents data, ax2ty
   in
-  (Refset.add obj curr, data, ax2ty)
+  (Refset_env.add obj curr, data, ax2ty)
+
+(** Collects the references occurring in the declaration of mutual inductive
+    definitions. All the constructors and names of a mutual inductive
+    definition share exactly the same dependencies. Also, there is no explicit
+    dependency between mutually defined inductives and constructors. *)
+and traverse_inductive (curr, data, ax2ty) mind obj =
+  let firstind_ref = (IndRef (mind, 0)) in
+  let label = label_of obj in
+  let data, ax2ty =
+   (* Invariant : I_0 \in data iff I_i \in data iff c_ij \in data
+      where I_0, I_1, ... are in the same mutual definition and c_ij
+      are all their constructors. *)
+   if Refmap_env.mem firstind_ref data then data, ax2ty else
+     let mib = Global.lookup_mind mind in
+     (* Collects references of parameters *)
+     let param_ctx = mib.mind_params_ctxt in
+     let nparam = List.length param_ctx in
+     let accu =
+       traverse_context label Context.Rel.empty
+                        (Refset_env.empty, data, ax2ty) param_ctx
+     in
+     (* Build the context of all arities *)
+     let arities_ctx =
+       let global_env = Global.env () in
+       Array.fold_left (fun accu oib ->
+          let pspecif = Univ.in_punivs (mib, oib) in
+          let ind_type = Inductive.type_of_inductive global_env pspecif in
+          let ind_name = Name oib.mind_typename in
+          Context.Rel.add (Context.Rel.Declaration.LocalAssum (ind_name, ind_type)) accu)
+          Context.Rel.empty mib.mind_packets
+     in
+     (* For each inductive, collects references in their arity and in the type
+        of constructors*)
+     let (contents, data, ax2ty) = Array.fold_left (fun accu oib ->
+         let arity_wo_param =
+           List.rev (List.skipn nparam (List.rev oib.mind_arity_ctxt))
+         in
+         let accu =
+           traverse_context
+             label param_ctx accu arity_wo_param
+         in
+         Array.fold_left (fun accu cst_typ ->
+            let param_ctx, cst_typ_wo_param = Term.decompose_prod_n_assum nparam cst_typ in
+            let ctx = Context.(Rel.fold_outside Context.Rel.add ~init:arities_ctx param_ctx) in
+            traverse label ctx accu cst_typ_wo_param)
+          accu oib.mind_user_lc)
+       accu mib.mind_packets
+     in
+     (* Maps all these dependencies to inductives and constructors*)
+     let data = Array.fold_left_i (fun n data oib ->
+       let ind = (mind, n) in
+       let data = Refmap_env.add (IndRef ind) contents data in
+       Array.fold_left_i (fun k data _ ->
+         Refmap_env.add (ConstructRef (ind, k+1)) contents data
+       ) data oib.mind_consnames) data mib.mind_packets
+     in
+     data, ax2ty
+  in
+  (Refset_env.add obj curr, data, ax2ty)
+
+(** Collects references in a rel_context. *)
+and traverse_context current ctx accu ctxt =
+  snd (Context.Rel.fold_outside (fun decl (ctx, accu) ->
+    match decl with
+     | Context.Rel.Declaration.LocalDef (_,c,t) ->
+          let accu = traverse current ctx (traverse current ctx accu t) c in
+          let ctx = Context.Rel.add decl ctx in
+          ctx, accu
+     | Context.Rel.Declaration.LocalAssum (_,t) ->
+          let accu = traverse current ctx accu t in
+          let ctx = Context.Rel.add decl ctx in
+           ctx, accu) ctxt ~init:(ctx, accu))
 
 let traverse current t =
   let () = modcache := MPmap.empty in
-  traverse current [] (Refset.empty, Refmap.empty, Refmap.empty) t
+  traverse current Context.Rel.empty (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
@@ -208,14 +282,14 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
   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
+    let decl = Global.lookup_named id in
+    if is_local_assum decl 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.find obj ax2ty with Not_found -> [] 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
@@ -227,4 +301,4 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
       accu
   | IndRef _ | ConstructRef _ -> accu
   in
-  Refmap.fold fold graph ContextObjectMap.empty
+  Refmap_env.fold fold graph ContextObjectMap.empty
diff --git a/toplevel/assumptions.mli b/toplevel/assumptions.mli
index a608fe5050..0726757839 100644
--- a/toplevel/assumptions.mli
+++ b/toplevel/assumptions.mli
@@ -1,12 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Names
 open Term
 open Globnames
@@ -21,8 +20,8 @@ open Printer
 *)
 val traverse :
   Label.t -> constr ->
-    (Refset.t * Refset.t Refmap.t *
-     (label * Context.rel_context * types) list Refmap.t)
+    (Refset_env.t * Refset_env.t Refmap_env.t *
+     (label * Context.Rel.t * 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
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index d1452fca21..3d053c2e1b 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -25,6 +25,7 @@ open Tactics
 open Ind_tables
 open Misctypes
 open Proofview.Notations
+open Context.Rel.Declaration
 
 let out_punivs = Univ.out_punivs
 
@@ -85,7 +86,7 @@ let destruct_on c = destruct false None c None None
 
 let destruct_on_using c id =
   destruct false None c
-    (Some (dl,[[dl,IntroNaming IntroAnonymous];
+    (Some (dl,IntroOrPattern [[dl,IntroNaming IntroAnonymous];
                [dl,IntroNaming (IntroIdentifier id)]]))
     None
 
@@ -102,7 +103,7 @@ let mkFullInd (ind,u) n =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   if nparrec > 0
     then mkApp (mkIndU (ind,u),
-      Array.of_list(extended_rel_list (nparrec+n) lnamesparrec))
+      Array.of_list(Context.Rel.to_extended_list (nparrec+n) lnamesparrec))
     else mkIndU (ind,u)
 
 let check_bool_is_defined () =
@@ -111,7 +112,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
@@ -137,7 +138,7 @@ let build_beq_scheme kn =
         | Name s -> Id.of_string ("eq_"^(Id.to_string s))
         | Anonymous -> Id.of_string "eq_A"
     in
-    let ext_rel_list = extended_rel_list 0 lnamesparrec in
+    let ext_rel_list = Context.Rel.to_extended_list 0 lnamesparrec in
       let lift_cnt = ref 0 in
       let eqs_typ = List.map (fun aa ->
                                 let a = lift !lift_cnt aa in
@@ -146,17 +147,17 @@ let build_beq_scheme kn =
                              ) ext_rel_list in
 
         let eq_input = List.fold_left2
-          ( fun a b (n,_,_) -> (* mkLambda(n,b,a) ) *)
+          ( fun a b decl -> (* mkLambda(n,b,a) ) *)
                 (* here I leave the Naming thingy so that the type of
                   the function is more readable for the user *)
-                mkNamedLambda (eqName n) b a )
+                mkNamedLambda (eqName (get_name decl)) b a )
                 c (List.rev eqs_typ) lnamesparrec
        in
-        List.fold_left (fun a (n,_,t) ->(* mkLambda(n,t,a)) eq_input rel_list *)
+        List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *)
           (* Same here , hoping the auto renaming will do something good ;)  *)
           mkNamedLambda
-                (match n with Name s -> s | Anonymous ->  Id.of_string "A")
-                t  a) eq_input lnamesparrec
+                (match get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
+                (get_type decl)  a) eq_input lnamesparrec
  in
  let make_one_eq cur =
   let u = Univ.Instance.empty in
@@ -179,23 +180,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
@@ -234,11 +234,11 @@ let build_beq_scheme kn =
                Cn => match Y with ... end |]  part *)
     let ci = make_case_info env (fst ind) MatchStyle in
     let constrs n = get_constructors env (make_ind_family (ind,
-      extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in
+      Context.Rel.to_extended_list (n+nb_ind-1) mib.mind_params_ctxt)) in
     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
@@ -249,14 +249,14 @@ let build_beq_scheme kn =
                     | 0 -> Lazy.force tt
                     | _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in
                       for ndx = 0 to nb_cstr_args-1 do
-                        let _,_,cc = List.nth constrsi.(i).cs_args ndx in
+                        let cc = get_type (List.nth constrsi.(i).cs_args ndx) in
                           let eqA, eff' = compute_A_equality rel_list
                                           nparrec
                                           (nparrec+3+2*nb_cstr_args)
                                           (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)|]
@@ -268,14 +268,14 @@ let build_beq_scheme kn =
                           (Array.sub eqs 1 (nb_cstr_args - 1))
                   )
    		  in
-		    (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) cc
+		    (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a)) cc
                     (constrsj.(j).cs_args)
 		)
-	      else ar2.(j) <- (List.fold_left (fun a (p,q,r) ->
-			mkLambda (p,r,a)) (Lazy.force ff) (constrsj.(j).cs_args) )
+	      else ar2.(j) <- (List.fold_left (fun a decl ->
+			mkLambda (get_name decl, get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) )
 	    done;
 
-	  ar.(i) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a))
+	  ar.(i) <- (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a))
 			(mkCase (ci,do_predicate rel_list nb_cstr_args,
 				  mkVar (Id.of_string "Y") ,ar2))
 			 (constrsi.(i).cs_args))
@@ -288,7 +288,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));
@@ -296,7 +296,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
@@ -304,7 +304,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
@@ -330,7 +330,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
@@ -355,12 +355,12 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
         )))
       )
   in
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
     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
@@ -385,10 +385,10 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
            Tacticals.New.tclTHENLIST [
              Proofview.tclEFFECTS eff;
              Equality.replace p q ; apply app ; Auto.default_auto]
-  end
+  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
@@ -417,7 +417,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
   let rec aux l1 l2 =
     match (l1,l2) with
     | (t1::q1,t2::q2) ->
-        Proofview.Goal.enter begin fun gl ->
+        Proofview.Goal.enter { enter = begin fun gl ->
         let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
         if eq_constr t1 t2 then aux q1 q2
         else (
@@ -458,7 +458,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
                   aux q1 q2 ]
               )
         )
-        end
+        end }
     | ([],[]) -> Proofview.tclUNIT ()
     | _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.")
   in
@@ -488,8 +488,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
   create, from a list of ids [i1,i2,...,in] the list
   [(in,eq_in,in_bl,in_al),,...,(i1,eq_i1,i1_bl_i1_al  )]
 *)
-let list_id l = List.fold_left ( fun a (n,_,t) -> let s' =
-      match n with
+let list_id l = List.fold_left ( fun a decl -> let s' =
+      match get_name decl with
         Name s -> Id.to_string s
       | Anonymous -> "A" in
           (Id.of_string s',Id.of_string ("eq_"^s'),
@@ -536,9 +536,9 @@ let compute_bl_goal ind lnamesparrec nparrec =
       let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
         mkNamedProd seq b a
       ) bl_input (List.rev list_id) (List.rev eqs_typ) in
-      List.fold_left (fun a (n,_,t) -> mkNamedProd
-                (match n with Name s -> s | Anonymous ->  Id.of_string "A")
-                t  a) eq_input lnamesparrec
+      List.fold_left (fun a decl -> mkNamedProd
+                (match get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
+                (get_type decl) a) eq_input lnamesparrec
     in
       let n = Id.of_string "x" and
           m = Id.of_string "y" in
@@ -551,7 +551,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 =
@@ -565,7 +565,7 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec =
           avoid := fresh::(!avoid); fresh
         end gl
       in
-      Proofview.Goal.nf_enter begin fun gl ->
+      Proofview.Goal.nf_enter { enter = begin fun gl ->
       let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
       let freshn = fresh_id (Id.of_string "x") gl in
       let freshm = fresh_id (Id.of_string "y") gl in
@@ -581,25 +581,25 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec =
                      Tacticals.New.tclTRY (
                       Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
                      );
-                     Proofview.V82.tactic (simpl_in_hyp (freshz,Locus.InHyp));
+                     simpl_in_hyp (freshz,Locus.InHyp);
 (*
 repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 *)
                     Tacticals.New.tclREPEAT (
                       Tacticals.New.tclTHENLIST [
                          Simple.apply_in freshz (andb_prop());
-                         Proofview.Goal.nf_enter begin fun gl ->
+                         Proofview.Goal.nf_enter { enter = begin fun gl ->
                            let fresht = fresh_id (Id.of_string "Z") gl in
-                            (destruct_on_as (mkVar freshz)
-                                  [[dl,IntroNaming (IntroIdentifier fresht);
+                            destruct_on_as (mkVar freshz)
+                                  (IntroOrPattern [[dl,IntroNaming (IntroIdentifier fresht);
                                     dl,IntroNaming (IntroIdentifier freshz)]])
-                         end
+                         end }
                         ]);
 (*
   Ci a1 ... an = Ci b1 ... bn
  replace bi with ai; auto || replace bi with ai by  apply typeofbi_prod ; auto
 *)
-                      Proofview.Goal.nf_enter begin fun gls ->
+                      Proofview.Goal.nf_enter { enter = begin fun gls ->
                         let gl = Proofview.Goal.concl gls in
                         match (kind_of_term gl) with
                         | App (c,ca) -> (
@@ -608,7 +608,7 @@ 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)))
@@ -618,14 +618,19 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                           | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.")
                         )
                         | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
-                      end
+                      end }
 
                     ]
-      end
+      end }
 
 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 ""
@@ -636,9 +641,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
 
@@ -673,9 +679,9 @@ let compute_lb_goal ind lnamesparrec nparrec =
       let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
         mkNamedProd seq b a
       ) lb_input (List.rev list_id) (List.rev eqs_typ) in
-      List.fold_left (fun a (n,_,t) -> mkNamedProd
-                (match n with Name s -> s | Anonymous ->  Id.of_string "A")
-                t  a) eq_input lnamesparrec
+      List.fold_left (fun a decl -> mkNamedProd
+                (match (get_name decl) with Name s -> s | Anonymous ->  Id.of_string "A")
+                (get_type decl)  a) eq_input lnamesparrec
     in
       let n = Id.of_string "x" and
           m = Id.of_string "y" in
@@ -688,7 +694,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 =
@@ -702,7 +708,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
           avoid := fresh::(!avoid); fresh
         end gl
       in
-      Proofview.Goal.nf_enter begin fun gl ->
+      Proofview.Goal.nf_enter { enter = begin fun gl ->
       let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
       let freshn = fresh_id (Id.of_string "x") gl in
       let freshm = fresh_id (Id.of_string "y") gl in
@@ -719,20 +725,20 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
                       Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None)
                      );
                      Equality.inj None false None (mkVar freshz,NoBindings);
-		     intros; (Proofview.V82.tactic simpl_in_concl);
+		     intros; simpl_in_concl;
                      Auto.default_auto;
                      Tacticals.New.tclREPEAT (
                       Tacticals.New.tclTHENLIST [apply (andb_true_intro());
                                   simplest_split ;Auto.default_auto ]
                       );
-                      Proofview.Goal.nf_enter begin fun gls ->
+                      Proofview.Goal.nf_enter { enter = begin fun gls ->
                         let gl = Proofview.Goal.concl gls in
                         (* assume the goal to be eq (eq_type ...) = true *)
                         match (kind_of_term gl) with
                         | 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)
@@ -741,13 +747,13 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
                         )
                         | _ ->
                             Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
-                      end
+                      end }
                     ]
-      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 ""
@@ -758,11 +764,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
 
@@ -813,9 +820,9 @@ let compute_dec_goal ind lnamesparrec nparrec =
       let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
         mkNamedProd seq b a
       ) bl_input (List.rev list_id) (List.rev eqs_typ) in
-      List.fold_left (fun a (n,_,t) -> mkNamedProd
-                (match n with Name s -> s | Anonymous ->  Id.of_string "A")
-                t  a) eq_input lnamesparrec
+      List.fold_left (fun a decl -> mkNamedProd
+                (match get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
+                (get_type decl) a) eq_input lnamesparrec
     in
       let n = Id.of_string "x" and
           m = Id.of_string "y" in
@@ -848,7 +855,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
       avoid := fresh::(!avoid); fresh
     end gl
   in
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
   let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
   let freshn = fresh_id (Id.of_string "x") gl in
   let freshm = fresh_id (Id.of_string "y") gl in
@@ -868,7 +875,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
     Not_found ->
       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;
@@ -879,7 +886,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
 	)
 	  (Tacticals.New.tclTHEN (destruct_on eqbnm) Auto.default_auto);
 
-        Proofview.Goal.nf_enter begin fun gl ->
+        Proofview.Goal.nf_enter { enter = begin fun gl ->
           let freshH2 = fresh_id (Id.of_string "H") gl in
 	  Tacticals.New.tclTHENS (destruct_on_using (mkVar freshH) freshH2) [
 	    (* left *)
@@ -891,11 +898,11 @@ let compute_dec_tact ind lnamesparrec nparrec =
             ;
 
 	    (*right *)
-            Proofview.Goal.nf_enter begin fun gl ->
+            Proofview.Goal.nf_enter { enter = begin fun gl ->
             let freshH3 = fresh_id (Id.of_string "H") gl in
             Tacticals.New.tclTHENLIST [
 	      simplest_right ;
-              Proofview.V82.tactic (unfold_constr (Lazy.force Coqlib.coq_not_ref));
+              unfold_constr (Lazy.force Coqlib.coq_not_ref);
               intro;
               Equality.subst_all ();
               assert_by (Name freshH3)
@@ -913,13 +920,13 @@ let compute_dec_tact ind lnamesparrec nparrec =
                               true;
               Equality.discr_tac false None
 	    ]
-            end
+            end }
 	  ]
-        end
+        end }
   ]
-  end
+  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
     raise DecidabilityMutualNotSupported;
@@ -927,14 +934,15 @@ let make_eq_decidability mind =
   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 20a3d5d74f..b6c66a1e84 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index accba3121b..4f3ffbcaee 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -110,6 +110,11 @@ let rec strip_wrapping_exceptions = function
     strip_wrapping_exceptions e
   | exc -> exc
 
+let additional_error_info = ref []
+
+let register_additional_error_info f =
+  additional_error_info := f :: !additional_error_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
@@ -120,19 +125,12 @@ let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc,
       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
+  let e' =
+    try Some (CList.find_map (fun f -> f e) !additional_error_info)
+    with _ -> None
+  in
+  match e' with
   | None -> e
-  | Some trace ->
-    let (e, info) = e in
-    match Himsg.extract_ltac_trace trace loc with
-    | None, loc -> (e, Loc.add_loc info loc)
-    | Some msg, loc ->
-      (EvaluatedError (msg, Some e), Loc.add_loc info loc)
-
-let _ = Tactic_debug.explain_logic_error :=
-  (fun e -> Errors.print (fst (process_vernac_interp_error (e, Exninfo.null))))
-
-let _ = Tactic_debug.explain_logic_error_no_anomaly :=
-  (fun e -> Errors.print_no_report (fst (process_vernac_interp_error (e, Exninfo.null))))
+  | Some (None, loc) -> (fst e, Loc.add_loc (snd e) loc)
+  | Some (Some msg, loc) ->
+    (EvaluatedError (msg, Some (fst e)), Loc.add_loc (snd e) loc)
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 729686f32d..a0e3e3c199 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -19,3 +19,4 @@ val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> U
 
 val explain_exn_default : exn -> Pp.std_ppcmds
 
+val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option * Loc.t) option) -> unit
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 0e270f960b..a9c53b4d4e 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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
@@ -196,20 +197,20 @@ let build_id_coercion idf_opt source poly =
   let val_f =
     it_mkLambda_or_LetIn
       (mkLambda (Name Namegen.default_dependent_ident,
-		 applistc vs (extended_rel_list 0 lams),
+		 applistc vs (Context.Rel.to_extended_list 0 lams),
 		 mkRel 1))
        lams
   in
   let typ_f =
     it_mkProd_wo_LetIn
-      (mkProd (Anonymous, applistc vs (extended_rel_list 0 lams), lift 1 t))
+      (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list 0 lams), lift 1 t))
       lams
   in
   (* juste pour verification *)
   let _ =
     if not
-      (Reductionops.is_conv_leq env Evd.empty
-	(Typing.unsafe_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/class.mli b/toplevel/class.mli
index bd6c7a6d12..5f9ae28f62 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 33891ad94c..235732b52c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -20,6 +20,8 @@ open Libnames
 open Globnames
 open Constrintern
 open Constrexpr
+open Sigma.Notations
+open Context.Rel.Declaration
 (*i*)
 
 open Decl_kinds
@@ -74,14 +76,14 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m
 
 let type_ctx_instance evars env ctx inst subst =
   let rec aux (subst, instctx) l = function
-    (na, b, t) :: ctx ->
-      let t' = substl subst t in
+    decl :: ctx ->
+      let t' = substl subst (get_type decl) in
       let c', l =
-	match b with
-	| None -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l
-	| Some b -> substl subst b, l
+	match decl with
+	| LocalAssum _ -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l
+	| LocalDef (_,b,_) -> substl subst b, l
       in
-      let d = na, Some c', t' in
+      let d = get_name decl, Some c', t' in
 	aux (c' :: subst, d :: instctx) l ctx
     | [] -> subst
   in aux (subst, []) inst (List.rev ctx)
@@ -101,32 +103,36 @@ let instance_hook k pri global imps ?hook cst =
   Typeclasses.declare_instance pri (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant k pri global imps ?hook id poly uctx term termtype =
+let declare_instance_constant k pri global imps ?hook id pl poly evm term termtype =
   let kind = IsDefinition Instance in
-  let uctx = 
+  let evm = 
     let levels = Univ.LSet.union (Universes.universes_of_constr termtype) 
 				 (Universes.universes_of_constr term) in
-      Universes.restrict_universe_context uctx levels 
+    Evd.restrict_universe_context evm levels 
   in
+  let pl, uctx = Evd.universe_context ?names:pl evm in
   let entry = 
-    Declare.definition_entry ~types:termtype ~poly ~univs:(Univ.ContextSet.to_context uctx) term
+    Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
   in
   let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
     Declare.definition_message id;
+    Universes.register_universe_binders (ConstRef kn) pl;
     instance_hook k pri global imps ?hook (ConstRef kn);
     id
 
-let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) props
+let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props
     ?(generalize=true)
     ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
-  let evars = ref (Evd.from_env env) in
+  let ((loc, instid), pl) = instid in
+  let uctx = Evd.make_evar_universe_context env pl in
+  let evars = ref (Evd.from_ctx uctx) in
   let tclass, ids =
     match bk with
     | Implicit ->
 	Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
-	  (fun avoid (clname, (id, _, t)) ->
+	  (fun avoid (clname, _) ->
 	    match clname with
 	    | Some (cl, b) ->
 		let t = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
@@ -149,16 +155,17 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
     let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
     let cl, u = Typeclasses.typeclass_univ_instance k in
     let _, args = 
-      List.fold_right (fun (na, b, t) (args, args') ->
-	match b with
-	| None -> (List.tl args, List.hd args :: args')
-	| Some b -> (args, substl args' b :: args'))
+      List.fold_right (fun decl (args, args') ->
+        let open Context.Rel.Declaration in
+	match decl with
+	| LocalAssum _ -> (List.tl args, List.hd args :: args')
+	| LocalDef (_,b,_) -> (args, substl args' b :: args'))
 	(snd cl.cl_context) (args, [])
     in
       cl, u, c', ctx', ctx, len, imps, args
   in
   let id =
-    match snd instid with
+    match instid with
 	Name id ->
 	  let sp = Lib.make_path id in
 	    if Nametab.exists_cci sp then
@@ -175,7 +182,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
     if abstract then
       begin
 	let subst = List.fold_left2
-	  (fun subst' s (_, b, _) -> if Option.is_empty b then s :: subst' else subst')
+	  (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
 	  [] subst (snd k.cl_context)
 	in
 	let (_, ty_constr) = instance_constructor (k,u) subst in
@@ -184,17 +191,19 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	  let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
 	    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 
+	Pretyping.check_evars env Evd.empty !evars termtype;
+	let pl, ctx = Evd.universe_context ?names:pl !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
+	in
+	  Universes.register_universe_binders (ConstRef cst) pl;
+	  instance_hook k pri global imps ?hook (ConstRef cst); id
       end
     else (
       let props =
 	match props with
-	| Some (true, CRecord (loc, _, fs)) ->
+	| Some (true, CRecord (loc, fs)) ->
 	    if List.length fs > List.length k.cl_props then
 	      mismatched_props env' (List.map snd fs) k.cl_props;
 	    Some (Inl fs)
@@ -217,10 +226,10 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	    in
 	    let props, rest =
 	      List.fold_left
-		(fun (props, rest) (id,b,_) ->
-		  if Option.is_empty b then 
+		(fun (props, rest) decl ->
+		  if is_local_assum decl then
 		    try
-		      let is_id (id', _) = match id, get_id id' with
+		      let is_id (id', _) = match get_name decl, get_id id' with
 			| Name id, (_, id') -> Id.equal id id'
 			| Anonymous, _ -> false
                       in
@@ -254,7 +263,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	    None, termtype
 	| Some (Inl subst) ->
 	  let subst = List.fold_left2
-	    (fun subst' s (_, b, _) -> if Option.is_empty b then s :: subst' else subst')
+	    (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
 	    [] subst (k.cl_props @ snd k.cl_context)
 	  in
 	  let (app, ty_constr) = instance_constructor (k,u) subst in
@@ -278,17 +287,16 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
       let evm, nf = Evarutil.nf_evar_map_universes !evars in
       let termtype = nf termtype in
       let _ = (* Check that the type is free of evars now. *)
-	Evarutil.check_evars env Evd.empty evm termtype
+	Pretyping.check_evars env Evd.empty evm termtype
       in
       let term = Option.map nf term in
 	if not (Evd.has_undefined evm) && not (Option.is_empty term) then
-          let ctx = Evd.universe_context_set evm in
-	  declare_instance_constant k pri global imps ?hook id 
-            poly ctx (Option.get term) termtype
-	else if !refine_instance || Option.is_empty term then begin
+	  declare_instance_constant k pri global imps ?hook id pl
+            poly evm (Option.get term) termtype
+	else if Flags.is_program_mode () || refine || Option.is_empty term then begin
 	  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	    if Flags.is_program_mode () then
-	      let hook vis gr =
+	      let hook vis gr _ =
 		let cst = match gr with ConstRef kn -> kn | _ -> assert false in
 		  Impargs.declare_manual_implicits false gr ~enriching:false [imps];
 		  Typeclasses.declare_instance pri (not global) (ConstRef cst)
@@ -304,7 +312,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
               let hook = Lemmas.mk_hook hook in
 	      let ctx = Evd.evar_universe_context evm in
 		ignore (Obligations.add_definition id ?term:constr
-			typ ctx ~kind:(Global,poly,Instance) ~hook obls);
+ 			?pl typ ctx ~kind:(Global,poly,Instance) ~hook obls);
 		id
 	    else
 	      (Flags.silently 
@@ -322,7 +330,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 		if not (Option.is_empty term) then
                   let init_refine =
                     Tacticals.New.tclTHENLIST [
-                      Proofview.Refine.refine (fun evm -> evm, Option.get term);
+                      Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) };
                       Proofview.Unsafe.tclNEWGOALS gls;
                       Tactics.New.reduce_after_refine;
                     ]
@@ -338,32 +346,36 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 let named_of_rel_context l =
   let acc, ctx =
     List.fold_right
-      (fun (na, b, t) (subst, ctx) ->
-	let id = match na with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
-	let d = (id, Option.map (substl subst) b, substl subst t) in
+      (fun decl (subst, ctx) ->
+        let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
+	let d = match decl with
+	  | LocalAssum (_,t) -> id, None, substl subst t
+	  | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
 	  (mkVar id :: subst, d :: ctx))
       l ([], [])
   in ctx
 
 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
-  let ce t = Evarutil.check_evars env Evd.empty !evars t in
-  let () = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx in
+  let fullctx = Context.Rel.map subst fullctx in
+  let ce t = Pretyping.check_evars env Evd.empty !evars t in
+  let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
   let ctx =
     try named_of_rel_context fullctx
     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 +391,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/classes.mli b/toplevel/classes.mli
index 2b7e9e4fe2..7beb873e63 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -1,13 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Names
-open Context
 open Environ
 open Constrexpr
 open Typeclasses
@@ -15,9 +14,9 @@ open Libnames
 
 (** Errors *)
 
-val mismatched_params : env -> constr_expr list -> rel_context -> 'a
+val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a
 
-val mismatched_props : env -> constr_expr list -> rel_context -> 'a
+val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
 
 (** Instance declaration *)
 
@@ -31,8 +30,9 @@ val declare_instance_constant :
   Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(Globnames.global_reference -> unit) ->
   Id.t -> (** name *)
+  Id.t Loc.located list option ->
   bool -> (* polymorphic *)
-  Univ.universe_context_set -> (* Universes *)
+  Evd.evar_map -> (* Universes *)
   Constr.t -> (** body *)
   Term.types -> (** type *)
   Names.Id.t
@@ -40,6 +40,7 @@ val declare_instance_constant :
 val new_instance :
   ?abstract:bool -> (** Not abstract by default. *)
   ?global:bool -> (** Not global by default. *)
+  ?refine:bool -> (** Allow refinement *)
   Decl_kinds.polymorphic ->
   local_binder list ->
   typeclass_constraint ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 04238da2bd..38bc0e568e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,7 +12,6 @@ open Util
 open Flags
 open Term
 open Vars
-open Context
 open Termops
 open Entries
 open Environ
@@ -37,17 +36,20 @@ open Evarconv
 open Indschemes
 open Misctypes
 open Vernacexpr
+open Sigma.Notations
+open Context.Rel.Declaration
+open Entries
 
-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 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 (LocalAssum (x,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 (LocalDef (x,b,t)) env) sigma f (n-1) c)
       | _ -> assert false
 
 let rec complete_conclusion a cs = function
@@ -67,39 +69,44 @@ 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
+      let (redfun, _) = reduction_of_red_expr env red in
+      let redfun env sigma c =
+        let sigma = Sigma.Unsafe.of_evar_map sigma in
+        let Sigma (c, _, _) = redfun.e_redfun env sigma c in
+        c
+      in
       { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out
-        (fun ((body,ctx),eff) ->
-          (under_binders env
-             (fst (reduction_of_red_expr env red)) n body,ctx),eff) }
+        (fun ((body,ctx),eff) -> (under_binders env sigma redfun 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
-	let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
+	let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
 	let env_bl = push_rel_context ctx env in
 	let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in
         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
-	let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
+	let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
 	let env_bl = push_rel_context ctx env in
 	let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in
 	let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
@@ -118,15 +125,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 (Context.Rel.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 +146,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 +159,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 +176,20 @@ 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
@@ -188,16 +200,18 @@ let do_definition ident k bl red_option c ctypopt hook =
 	Obligations.eterm_obligations env ident evd 0 c typ
       in
       let ctx = Evd.evar_universe_context evd in
+      let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in
 	ignore(Obligations.add_definition
-          ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
+          ident ~term:c cty ctx ?pl ~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 +238,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 +255,18 @@ 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 open Context.Named.Declaration in
   let env = Global.env () in
   let evdref = ref (Evd.from_env env) in
   let l = 
@@ -262,7 +281,7 @@ let do_assumptions (_, poly, _ as kind) nl l =
   let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) ->
     let (t,ctx),imps = interp_assumption evdref env ienv [] c in
     let env =
-      push_named_context (List.map (fun (_,id) -> (id,None,t)) idl) env in
+      push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in
     let ienv = List.fold_right (fun (_,id) ienv ->
       let impls = compute_internalization_data env Variable t imps in
       Id.Map.add id impls ienv) idl ienv in
@@ -273,23 +292,63 @@ 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 *)
 
 let push_types env idl tl =
-  List.fold_left2 (fun env id t -> Environ.push_rel (Name id,None,t) env)
+  List.fold_left2 (fun env id t -> Environ.push_rel (LocalAssum (Name id,t)) env)
     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
 }
@@ -327,8 +386,8 @@ let mk_mltype_data evdref env assums arity indname =
   (is_ml_type,indname,assums)
 
 let prepare_param = function
-  | (na,None,t) -> out_name na, LocalAssum t
-  | (na,Some b,_) -> out_name na, LocalDef b
+  | LocalAssum (na,t) -> out_name na, LocalAssumEntry t
+  | LocalDef (na,b,_) -> out_name na, LocalDefEntry b
 
 (** Make the arity conclusion flexible to avoid generating an upper bound universe now,
     only if the universe does not appear anywhere else.
@@ -382,12 +441,12 @@ let interp_cstrs evdref env impls mldata arity ind =
 
 let sign_level env evd sign =
   fst (List.fold_right
-    (fun (_,b,t as d) (lev,env) ->
-      match b with
-      | Some _ -> (lev, push_rel d env)
-      | None ->
+    (fun d (lev,env) ->
+      match d with
+      | LocalDef _ -> lev, push_rel d env
+      | LocalAssum _ ->
 	let s = destSort (Reduction.whd_betadeltaiota env 
-			    (nf_evar evd (Retyping.get_type_of env evd t)))
+			    (nf_evar evd (Retyping.get_type_of env evd (get_type d))))
 	in
 	let u = univ_of_sort s in
 	  (Univ.sup u lev, push_rel d env))
@@ -398,7 +457,7 @@ let sup_list min = List.fold_left Univ.sup min
 let extract_level env evd min tys = 
   let sorts = List.map (fun ty -> 
     let ctx, concl = Reduction.dest_prod_assum env ty in
-      sign_level env evd ((Anonymous, None, concl) :: ctx)) tys 
+      sign_level env evd (LocalAssum (Anonymous, concl) :: ctx)) tys
   in sup_list min sorts
 
 let is_flexible_sort evd u =
@@ -465,16 +524,17 @@ let inductive_levels env evdref poly arities inds =
 	    Evd.set_leq_sort env evd (Prop Pos) du
 	  else evd
 	in
-	  (* let arity = it_mkProd_or_LetIn (mkType cu) ctx 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
-		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))
+	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
 
@@ -494,15 +554,17 @@ 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
+  let assums = List.filter is_local_assum ctx_params in
+  let params = List.map (fun decl -> out_name (get_name decl)) assums in
 
   (* Interpret the arities *)
   let arities = List.map (interp_ind_arity env_params evdref) indl in
@@ -513,7 +575,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
 
   (* Compute interpretation metadatas *)
   let indimpls = List.map (fun (_, _, impls) -> userimpls @ 
-    lift_implicits (rel_context_nhyps ctx_params) impls) arities in
+    lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
   let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
   let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
@@ -539,10 +601,11 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   let nf x = nf' (nf x) in
   let arities = List.map nf' arities in
   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 ctx_params = Context.Rel.map 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;
+  Context.Rel.iter (check_evars env0 Evd.empty evd) ctx_params;
   List.iter (fun (_,ctyps,_) ->
     List.iter (check_evars env_ar_params Evd.empty evd) ctyps)
     constructors;
@@ -556,7 +619,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     mind_entry_lc = ctypes
   }) indl arities aritypoly constructors in
   let impls =
-    let len = rel_context_nhyps ctx_params in
+    let len = Context.Rel.nhyps ctx_params in
       List.map2 (fun indimpls (_,_,cimpls) ->
 	indimpls, List.map (fun impls ->
 	  userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
@@ -568,8 +631,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 =
@@ -590,8 +653,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
@@ -618,7 +681,7 @@ 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
@@ -633,12 +696,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);
@@ -653,14 +719,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...
@@ -739,6 +805,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;
@@ -763,11 +830,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
@@ -809,19 +877,20 @@ let well_founded = init_constant ["Init"; "Wf"] "well_founded"
 let mkSubset name typ prop =
   mkApp (Universes.constr_of_global (delayed_force build_sigma).typ,
 	 [| typ; mkLambda (name, typ, prop) |])
-let sigT = Lazy.lazy_from_fun build_sigma_type
+let sigT = Lazy.from_fun build_sigma_type
 
 let make_qref s = Qualid (Loc.ghost, qualid_of_string s)
 let lt_ref = make_qref "Init.Peano.lt"
 
 let rec telescope = function
   | [] -> assert false
-  | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1
-  | (n, None, t) :: tl ->
+  | [LocalAssum (n, t)] -> t, [LocalDef (n, mkRel 1, t)], mkRel 1
+  | LocalAssum (n, t) :: tl ->
       let ty, tys, (k, constr) =
 	List.fold_left
-	  (fun (ty, tys, (k, constr)) (n, b, t) ->
-	    let pred = mkLambda (n, t, ty) in
+	  (fun (ty, tys, (k, constr)) decl ->
+            let t = get_type decl in
+            let pred = mkLambda (get_name decl, t, ty) in
 	    let ty = Universes.constr_of_global (Lazy.force sigT).typ in
 	    let intro = Universes.constr_of_global (Lazy.force sigT).intro in
 	    let sigty = mkApp (ty, [|t; pred|]) in
@@ -830,26 +899,27 @@ let rec telescope = function
 	  (t, [], (2, mkRel 1)) tl
       in
       let (last, subst) = List.fold_right2
-	(fun pred (n, b, t) (prev, subst) ->
+        (fun pred decl (prev, subst) ->
+          let t = get_type decl in
 	  let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in
 	  let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in
 	  let proj1 = applistc p1 [t; pred; prev] in
 	  let proj2 = applistc p2 [t; pred; prev] in
-	    (lift 1 proj2, (n, Some proj1, t) :: subst))
+	    (lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
 	(List.rev tys) tl (mkRel 1, [])
-      in ty, ((n, Some last, t) :: subst), constr
+      in ty, (LocalDef (n, last, t) :: subst), constr
 
-  | (n, Some b, t) :: tl -> let ty, subst, term = telescope tl in
-      ty, ((n, Some b, t) :: subst), lift 1 term
+  | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope tl in
+      ty, (LocalDef (n, b, t) :: subst), lift 1 term
 
 let nf_evar_context sigma ctx =
-  List.map (fun (n, b, t) ->
-    (n, Option.map (Evarutil.nf_evar sigma) b, Evarutil.nf_evar sigma t)) ctx
+  List.map (map_constr (Evarutil.nf_evar sigma)) ctx
 
-let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
+let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   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 _, ((env', binders_rel), impls) = interp_context_evars env evdref bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
@@ -857,7 +927,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
   let argtyp, letbinders, make = telescope binders_rel in
   let argname = Id.of_string "recarg" in
-  let arg = (Name argname, None, argtyp) in
+  let arg = LocalAssum (Name argname, argtyp) in
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
   let rel, _ = interp_constr_evars_impls env evdref r in
@@ -872,7 +942,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
       try
 	let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in
 	  match ctx, kind_of_term ar with
-	  | [(_, None, t); (_, None, u)], Sort (Prop Null)
+	  | [LocalAssum (_,t); LocalAssum (_,u)], Sort (Prop Null)
 	      when Reductionops.is_conv env !evdref t u -> t
 	  | _, _ -> error ()
       with e when Errors.noncritical e -> error ()
@@ -892,9 +962,9 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   in
   let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in
   let argid' = Id.of_string (Id.to_string argname ^ "'") in
-  let wfarg len = (Name argid', None,
-  		   mkSubset (Name argid') argtyp
-		    (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
+  let wfarg len = LocalAssum (Name argid',
+                              mkSubset (Name argid') argtyp
+				       (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
   in
   let intern_bl = wfarg 1 :: [arg] in
   let _intern_env = push_rel_context intern_bl env in
@@ -908,22 +978,22 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   (* substitute the projection of wfarg for something,
      now intern_arity is in wfarg :: arg *)
   let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
-  let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in
+  let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in
   let curry_fun =
     let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
     let intro = (*FIXME*)Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro in
     let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
     let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
     let rcurry = mkApp (rel, [| measure; lift len measure |]) in
-    let lam = (Name (Id.of_string "recproof"), None, rcurry) in
+    let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in
     let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
     let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
-      (Name recname, Some body, ty)
+      LocalDef (Name recname, body, ty)
   in
   let fun_bl = intern_fun_binder :: [arg] in
   let lift_lets = Termops.lift_rel_context 1 letbinders in
   let intern_body =
-    let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in
+    let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in
     let (r, l, impls, scopes) =
       Constrintern.compute_internalization_data env
 	Constrintern.Recursive full_arity impls 
@@ -943,7 +1013,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	       ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
 	     prop |])
   in
-  let def = Typing.solve_evars env evdref def in
+  let def = Typing.e_solve_evars env evdref def in
   let _ = evdref := Evarutil.nf_evar_map !evdref in
   let def = mkApp (def, [|intern_body_lam|]) in
   let binders_rel = nf_evar_context !evdref binders_rel in
@@ -952,12 +1022,12 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   let hook, recname, typ = 
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
-      let hook l gr = 
+      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 ?names:pl !evdref in
 	  (*FIXME poly? *)
-	let ce = definition_entry ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
+	let ce = definition_entry ~poly ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
 	(** FIXME: include locality *)
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
@@ -968,7 +1038,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	hook, name, typ
     else 
       let typ = it_mkProd_or_LetIn top_arity binders_rel in
-      let hook l gr = 
+      let hook l gr _ = 
 	if Impargs.is_implicit_args () || not (List.is_empty impls) then
 	  Impargs.declare_manual_implicits false gr [impls]
       in hook, recname, typ
@@ -981,15 +1051,26 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
     Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp 
   in
   let ctx = Evd.evar_universe_context !evdref in
-    ignore(Obligations.add_definition recname ~term:evars_def 
+    ignore(Obligations.add_definition recname ~term:evars_def ?pl
 	     evars_typ ctx evars ~hook)
 
 let interp_recursive isfix fixl notations =
+  let open Context.Named.Declaration in
   let env = Global.env() in
   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
@@ -1007,11 +1088,11 @@ let interp_recursive isfix fixl notations =
 	   let fixprot =
 	     try 
 	       let app = mkApp (delayed_force fix_proto, [|sort; t|]) in
-		 Typing.solve_evars env evdref app
+		 Typing.e_solve_evars env evdref app
 	     with e  when Errors.noncritical e -> t
 	   in
-	     (id,None,fixprot) :: env'
-	 else (id,None,t) :: env')
+	     LocalAssum (id,fixprot) :: env'
+	 else LocalAssum (id,t) :: env')
       [] fixnames fixtypes
   in
   let env_rec = push_named_context rec_sign env in
@@ -1033,10 +1114,10 @@ let interp_recursive isfix fixl notations =
   let evd, nf = nf_evars_and_universes evd in
   let fixdefs = List.map (Option.map nf) fixdefs in
   let fixtypes = List.map nf fixtypes in
-  let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in
+  let fixctxnames = List.map (fun (_,ctx) -> List.map get_name 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);
@@ -1046,27 +1127,28 @@ 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 =
-      List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+      List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
     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
@@ -1079,11 +1161,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 Univ.UContext.empty 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;
@@ -1091,30 +1173,33 @@ 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 =
-      List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+      List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
     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 Univ.UContext.empty 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
@@ -1130,15 +1215,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
@@ -1147,7 +1234,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 *)
@@ -1186,22 +1273,22 @@ let do_program_recursive local p fixkind fixl ntns =
   | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
   | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
   in
-  Obligations.add_mutual_definitions defs ~kind ctx ntns fixkind
+  Obligations.add_mutual_definitions defs ~kind ?pl ctx ntns fixkind
 
 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),pl),_,bl,typ,def),ntn)] ->
 	let recarg = 
 	  match n with
 	  | Some n -> mkIdentC (snd n)
 	  | None ->
 	      errorlabstrm "do_program_fixpoint"
 		(str "Recursive argument required for well-founded fixpoints")
-	in build_wellfounded (id, n, bl, typ, out_def def) r recarg ntn
+	in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn
 	     
-    | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
-	build_wellfounded (id, n, bl, typ, out_def def)
+    | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] ->
+	build_wellfounded (id, pl, n, bl, typ, out_def def) poly
 	  (Option.default (CRef (lt_ref,None)) r) m ntn
 	  
     | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
@@ -1217,9 +1304,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 3a38e52cee..b97cb487d5 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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 f0cac72d0a..b81c8da718 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -130,6 +130,7 @@ 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
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index c019cc1ced..4ff87628c8 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index caaf8054b8..063ed89643 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 8ed661e674..00554da308 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 3c87533a93..f46b901116 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -35,7 +35,7 @@ let print_header () =
   ppnl (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
   pp_flush ()
 
-let warning s = msg_warning (strbrk s)
+let warning s = with_option Flags.warn msg_warning (strbrk s)
 
 let toploop = ref None
 
@@ -144,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
@@ -162,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
@@ -171,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
@@ -185,9 +192,14 @@ 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 add_compat_require v =
+  match v with
+  | Flags.V8_4 -> add_require "Coq.Compat.Coq84"
+  | _ -> ()
 
 let compile_list = ref ([] : (bool * string) list)
 
@@ -226,15 +238,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 () =
@@ -254,18 +257,19 @@ let set_emacs () =
 *)
 
 let init_gc () =
-  let param =
-    try ignore (Sys.getenv "OCAMLRUNPARAM"); true
-    with Not_found -> false
-  in
-  let control = Gc.get () in
-  let tweaked_control = { control with
-    Gc.minor_heap_size = 33554432; (** 4M *)
-(*     Gc.major_heap_increment = 268435456; (** 32M *) *)
-    Gc.space_overhead = 120;
-  } in
-  if param then ()
-  else Gc.set tweaked_control
+  try
+    (* OCAMLRUNPARAM environment variable is set.
+     * In that case, we let ocamlrun to use the values provided by the user.
+     *)
+    ignore (Sys.getenv "OCAMLRUNPARAM")
+
+  with Not_found ->
+    (* OCAMLRUNPARAM environment variable is not set.
+     * In this case, we put in place our preferred configuration.
+     *)
+    Gc.set { (Gc.get ()) with
+             Gc.minor_heap_size = 33554432; (** 4M *)
+             Gc.space_overhead = 120}
 
 (*s Parsing of the command line.
     We no longer use [Arg.parse], in order to use share [Usage.print_usage]
@@ -352,7 +356,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);
@@ -438,10 +443,6 @@ let parse_args arglist =
       end
     |"-R" ->
       begin match rem with
-      | d :: "-as" :: [] -> error_missing_arg opt
-      | d :: "-as" :: p :: rem ->
-        warning "option -R * -as * deprecated, remove the -as";
-        set_include d p true; args := rem
       | d :: p :: rem -> set_include d p true; args := rem
       | _ -> error_missing_arg opt
       end
@@ -476,7 +477,7 @@ let parse_args arglist =
     |"-async-proofs-private-flags" ->
         Flags.async_proofs_private_flags := Some (next ());
     |"-worker-id" -> set_worker_id opt (next ())
-    |"-compat" -> Flags.compat_version := get_compat_version (next ())
+    |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v
     |"-compile" -> add_compile false (next ())
     |"-compile-verbose" -> add_compile true (next ())
     |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true
@@ -541,8 +542,8 @@ 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
+    |"-xml" -> Flags.xml_export := true
 
     (* Deprecated options *)
     |"-byte" -> warning "option -byte deprecated, call with .byte suffix"
@@ -558,7 +559,6 @@ let parse_args arglist =
     |"-force-load-proofs" -> warning "Obsolete option \"-force-load-proofs\"."
     |"-unsafe" -> warning "Obsolete option \"-unsafe\"."; ignore (next ())
     |"-quality" -> warning "Obsolete option \"-quality\"."
-    |"-xml" -> warning "Obsolete option \"-xml\"."
 
     (* Unknown option *)
     | s -> extras := s :: !extras
@@ -573,7 +573,7 @@ let parse_args arglist =
       else fatal_error (Errors.print e) false
     | any -> fatal_error (Errors.print any) (Errors.is_anomaly any)
 
-let init arglist =
+let init_toplevel arglist =
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
   Lib.init();
@@ -601,7 +601,6 @@ let init arglist =
       if_verbose print_header ();
       inputstate ();
       Mltop.init_known_plugins ();
-      set_vm_opt ();
       engage ();
       (* Be careful to set these variables after the inputstate *)
       Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
@@ -638,8 +637,6 @@ let init arglist =
     exit 0
   end
 
-let init_toplevel = init
-
 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,
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 356ccdcc69..c9d1ba45d5 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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 7d5d61fb8b..ffa11679c2 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,20 +9,22 @@
 open Names
 open Errors
 open Util
-open Context
 open Term
 open Vars
 open Entries
 open Declarations
 open Cooking
+open Entries
+open Context.Rel.Declaration
 
 (********************************)
 (* Discharging mutual inductive *)
 
-let detype_param = function
-  | (Name id,None,p) -> id, Entries.LocalAssum p
-  | (Name id,Some p,_) -> id, Entries.LocalDef p
-  | (Anonymous,_,_) -> anomaly (Pp.str "Unnamed inductive local variable")
+let detype_param =
+  function
+  | LocalAssum (Name id, p) -> id, LocalAssumEntry p
+  | LocalDef (Name id, p,_) -> id, LocalDefEntry p
+  | _ -> anomaly (Pp.str "Unnamed inductive local variable")
 
 (* Replace
 
@@ -37,8 +39,8 @@ let detype_param = function
 
 let abstract_inductive hyps nparams inds =
   let ntyp = List.length inds in
-  let nhyp = named_context_length hyps in
-  let args = instance_from_named_context (List.rev hyps) in
+  let nhyp = Context.Named.length hyps in
+  let args = Context.Named.to_instance (List.rev hyps) in
   let args = Array.of_list args in
   let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in
   let inds' =
@@ -53,7 +55,7 @@ let abstract_inductive hyps nparams inds =
 (* To be sure to be the same as before, should probably be moved to process_inductive *)
   let params' = let (_,arity,_,_,_) = List.hd inds' in
 		let (params,_) = decompose_prod_n_assum nparams' arity in
-		  List.map detype_param params
+                List.map detype_param params
   in
   let ind'' =
   List.map
@@ -100,7 +102,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
 	   Array.to_list mip.mind_consnames,
 	   Array.to_list lc))
       mib.mind_packets in
-  let sechyps' = map_named_context (expmod_constr modlist) sechyps in
+  let sechyps' = Context.Named.map (expmod_constr modlist) sechyps in
   let (params',inds') = abstract_inductive sechyps' nparams inds in
   let abs_ctx = Univ.instantiate_univ_context abs_ctx in
   let univs = Univ.UContext.union abs_ctx univs in
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 386e4e3ef8..18d1b67766 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -1,15 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Context
 open Declarations
 open Entries
 open Opaqueproof
 
 val process_inductive :
-  named_context Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+  Context.Named.t Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4
deleted file mode 100644
index 24661e124c..0000000000
--- a/toplevel/g_obligations.ml4
+++ /dev/null
@@ -1,135 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-(*
-  Syntax for the subtac terms and types.
-  Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
-
-
-open Libnames
-open Constrexpr
-open Constrexpr_ops
-
-(* We define new entries for programs, with the use of this module
- * Subtac. These entries are named Subtac.<foo>
- *)
-
-module Gram = Pcoq.Gram
-module Vernac = Pcoq.Vernac_
-module Tactic = Pcoq.Tactic
-
-open Pcoq
-
-let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
-
-type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
-
-let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
-  Genarg.create_arg None "withtac"
-
-let withtac = Pcoq.create_generic_entry "withtac" (Genarg.rawwit wit_withtac)
-
-GEXTEND Gram
-  GLOBAL: withtac;
-
-  withtac:
-    [ [ "with"; t = Tactic.tactic -> Some t
-      | -> None ] ]
-  ;
-
-  Constr.closed_binder:
-    [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
-	  let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
-          [LocalRawAssum ([id], default_binder_kind, typ)]
-    ] ];
-
-  END
-
-open Obligations
-
-let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
-
-VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl
-| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] ->
-    [ obligation (num, Some name, Some t) tac ]
-| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
-    [ obligation (num, Some name, None) tac ]
-| [ "Obligation" integer(num) ":" lconstr(t) withtac(tac) ] ->
-    [ obligation (num, None, Some t) tac ]
-| [ "Obligation" integer(num) withtac(tac) ] ->
-    [ obligation (num, None, None) tac ]
-| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
-    [ next_obligation (Some name) tac ]
-| [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ]
-END
-
-VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
-| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] ->
-    [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ]
-| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] ->
-    [ try_solve_obligation num None (Some (Tacinterp.interp t)) ]
-END
-
-VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF
-| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] ->
-    [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ]
-| [ "Solve" "Obligations" "with" tactic(t) ] ->
-    [ try_solve_obligations None (Some (Tacinterp.interp t)) ]
-| [ "Solve" "Obligations" ] ->
-    [ try_solve_obligations None None ]
-END
-
-VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF
-| [ "Solve" "All" "Obligations" "with" tactic(t) ] ->
-    [ solve_all_obligations (Some (Tacinterp.interp t)) ]
-| [ "Solve" "All" "Obligations" ] ->
-    [ solve_all_obligations None ]
-END
-
-VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF
-| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ]
-| [ "Admit" "Obligations" ] -> [ admit_obligations None ]
-END
-
-VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
-| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
-    set_default_tactic
-      (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
-      (Tacintern.glob_tactic t) ]
-END
-
-open Pp
-
-VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
-| [ "Show" "Obligation" "Tactic" ] -> [
-    msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ]
-END
-
-VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
-| [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ]
-| [ "Obligations" ] -> [ show_obligations None ]
-END
-
-VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY
-| [ "Preterm" "of" ident(name) ] -> [ msg_info (show_term (Some name)) ]
-| [ "Preterm" ] -> [ msg_info (show_term None) ]
-END
-
-open Pp
-
-(* Declare a printer for the content of Program tactics *)
-let () =
-  let printer _ _ _ = function
-  | None -> mt ()
-  | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac
-  in
-  (* should not happen *)
-  let dummy _ _ _ expr = assert false in
-  Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 7a3bcfba80..ad848ccfc8 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -23,22 +23,26 @@ open Cases
 open Logic
 open Printer
 open Evd
+open Context.Rel.Declaration
 
 (* This simplifies the typing context of Cases clauses *)
 (* hope it does not disturb other typing contexts *)
 let contract env lc =
   let l = ref [] in
-  let contract_context (na,c,t) env =
-    match c with
-      | Some c' when isRel c' ->
+  let contract_context decl env =
+    match decl with
+      | LocalDef (_,c',_) when isRel c' ->
           l := (Vars.substl !l c') :: !l;
           env
       | _ ->
-          let t' = Vars.substl !l t in
-          let c' = Option.map (Vars.substl !l) c in
-          let na' = named_hd env t' na in
+          let t' = Vars.substl !l (get_type decl) in
+          let c' = Option.map (Vars.substl !l) (get_value decl) in
+          let na' = named_hd env t' (get_name decl) in
           l := (mkRel 1) :: List.map (Vars.lift 1) !l;
-          push_rel (na',c',t') env in
+          match c' with
+          | None -> push_rel (LocalAssum (na',t')) env
+          | Some c' -> push_rel (LocalDef (na',c',t')) env
+  in
   let env = process_rel_context contract_context env in
   (env, List.map (Vars.substl !l) lc)
 
@@ -72,6 +76,15 @@ let rec contract3' env a b c = function
       let y,x = contract3' env a b c x in
       y,CannotSolveConstraint ((pb,env,t,u),x)
 
+(** Ad-hoc reductions *)
+
+let j_nf_betaiotaevar sigma j =
+  { uj_val = Evarutil.nf_evar sigma j.uj_val;
+    uj_type = Reductionops.nf_betaiota sigma j.uj_type }
+
+let jv_nf_betaiotaevar sigma jl =
+  Array.map (j_nf_betaiotaevar sigma) jl
+
 (** Printers *)
 
 let pr_lconstr c = quote (pr_lconstr c)
@@ -136,9 +149,9 @@ let pr_explicit env sigma t1 t2 = pr_explicit_aux env sigma t1 t2 explicit_flags
 
 let pr_db env i =
   try
-    match lookup_rel i env with
-        Name id, _, _ -> pr_id id
-      | Anonymous, _, _ -> str "<>"
+    match lookup_rel i env |> get_name with
+      | Name id -> pr_id id
+      | Anonymous -> str "<>"
   with Not_found -> str "UNBOUND_REL_" ++ int i
 
 let explain_unbound_rel env sigma n =
@@ -260,7 +273,7 @@ let explain_generalization env sigma (name,var) j =
   str "it has type" ++ spc () ++ pt ++
   spc () ++ str "which should be Set, Prop or Type."
 
-let rec explain_unification_error env sigma p1 p2 = function
+let explain_unification_error env sigma p1 p2 = function
   | None -> mt()
   | Some e ->
      let rec aux p1 p2 = function
@@ -318,7 +331,7 @@ let rec explain_unification_error env sigma p1 p2 = function
 
 let explain_actual_type env sigma j t reason =
   let env = make_all_name_different env in
-  let j = Evarutil.j_nf_betaiotaevar sigma j in
+  let j = j_nf_betaiotaevar sigma j in
   let t = Reductionops.nf_betaiota sigma t in
   (** Actually print *)
   let pe = pr_ne_context_of (str "In environment") env sigma in
@@ -333,7 +346,7 @@ let explain_actual_type env sigma j t reason =
   ppreason ++ str ".")
 
 let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
-  let randl = Evarutil.jv_nf_betaiotaevar sigma randl in
+  let randl = jv_nf_betaiotaevar sigma randl in
   let exptyp = Evarutil.nf_evar sigma exptyp in
   let actualtyp = Reductionops.nf_betaiota sigma actualtyp in
   let rator = Evarutil.j_nf_evar sigma rator in
@@ -775,7 +788,7 @@ let explain_unsatisfiable_constraints env sigma constr comp =
     explain_typeclass_resolution env sigma info k ++ fnl () ++ cstr
 
 let explain_pretype_error env sigma err =
-  let env = Evarutil.env_nf_betaiotaevar sigma env in
+  let env = Evardefine.env_nf_betaiotaevar sigma env in
   let env = make_all_name_different env in
   match err with
   | CantFindCaseType c -> explain_cant_find_case_type env sigma c
@@ -783,7 +796,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
@@ -822,7 +835,7 @@ let explain_not_match_error = function
   | ModuleTypeFieldExpected ->
     strbrk "a module type is expected"
   | NotConvertibleInductiveField id | NotConvertibleConstructorField id ->
-    str "types given to " ++ str (Id.to_string id) ++ str " differ"
+    str "types given to " ++ pr_id id ++ str " differ"
   | NotConvertibleBodyField ->
     str "the body of definitions differs"
   | NotConvertibleTypeField (env, typ1, typ2) ->
@@ -847,7 +860,7 @@ let explain_not_match_error = function
   | RecordProjectionsExpected nal ->
     (if List.length nal >= 2 then str "expected projection names are "
      else str "expected projection name is ") ++
-    pr_enum (function Name id -> str (Id.to_string id) | _ -> str "_") nal
+    pr_enum (function Name id -> pr_id id | _ -> str "_") nal
   | NotEqualInductiveAliases ->
     str "Aliases to inductive types do not match"
   | NoTypeConstraintExpected ->
@@ -890,17 +903,27 @@ let explain_is_a_functor () =
   str "Illegal use of a functor."
 
 let explain_incompatible_module_types mexpr1 mexpr2 =
-  str "Incompatible module types."
+  let open Declarations in
+  let rec get_arg = function
+  | NoFunctor _ -> 0
+  | MoreFunctor (_, _, ty) -> succ (get_arg ty)
+  in
+  let len1 = get_arg mexpr1.mod_type in
+  let len2 = get_arg mexpr2.mod_type in
+  if len1 <> len2 then
+    str "Incompatible module types: module expects " ++ int len2 ++
+      str " arguments, found " ++ int len1 ++ str "."
+  else str "Incompatible module types."
 
 let explain_not_equal_module_paths mp1 mp2 =
   str "Non equal modules."
 
 let explain_no_such_label l =
-  str "No such label " ++ str (Label.to_string l) ++ str "."
+  str "No such label " ++ pr_label l ++ str "."
 
 let explain_incompatible_labels l l' =
   str "Opening and closing labels are not the same: " ++
-  str (Label.to_string l) ++ str " <> " ++ str (Label.to_string l') ++ str "!"
+  pr_label l ++ str " <> " ++ pr_label l' ++ str "!"
 
 let explain_not_a_module s =
   quote (str s) ++ str " is not a module."
@@ -909,23 +932,26 @@ let explain_not_a_module_type s =
   quote (str s) ++ str " is not a module type."
 
 let explain_not_a_constant l =
-  quote (Label.print l) ++ str " is not a constant."
+  quote (pr_label l) ++ str " is not a constant."
 
 let explain_incorrect_label_constraint l =
   str "Incorrect constraint for label " ++
-  quote (Label.print l) ++ str "."
+  quote (pr_label l) ++ str "."
 
 let explain_generative_module_expected l =
-  str "The module " ++ str (Label.to_string l) ++ str " is not generative." ++
+  str "The module " ++ pr_label l ++ str " is not generative." ++
   strbrk " Only components of generative modules can be changed" ++
   strbrk " using the \"with\" construct."
 
 let explain_label_missing l s =
-  str "The field " ++ str (Label.to_string l) ++ str " is missing in "
+  str "The field " ++ pr_label l ++ str " is missing in "
   ++ str s ++ str "."
 
-let explain_higher_order_include () =
-  str "You cannot Include a higher-order structure."
+let explain_include_restricted_functor mp =
+  let q = Nametab.shortest_qualid_of_module mp in
+  str "Cannot include the functor " ++ Libnames.pr_qualid q ++
+  strbrk " since it has a restricted signature. " ++
+  strbrk "You may name first an instance of this functor, and include it."
 
 let explain_module_error = function
   | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err
@@ -943,7 +969,7 @@ 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 ()
+  | IncludeRestrictedFunctor mp -> explain_include_restricted_functor mp
 
 (* Module internalization errors *)
 
@@ -1194,7 +1220,7 @@ let explain_unused_clause env pats =
 let explain_non_exhaustive env pats =
   str "Non exhaustive pattern-matching: no clause found for " ++
   str (String.plural (List.length pats) "pattern") ++
-  spc () ++ hov 0 (pr_sequence pr_cases_pattern pats)
+  spc () ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats)
 
 let explain_cannot_infer_predicate env sigma typs =
   let env = make_all_name_different env in
@@ -1227,77 +1253,3 @@ let explain_reduction_tactic_error = function
       quote (pr_goal_concl_style_env env sigma c) ++
       spc () ++ str "is not well typed." ++ fnl () ++
       explain_type_error env' Evd.empty e
-
-let is_defined_ltac trace =
-  let rec aux = function
-  | (_, Proof_type.LtacNameCall f) :: tail ->
-      not (Tacenv.is_ltac_for_ml_tactic f)
-  | (_, Proof_type.LtacAtomCall _) :: tail ->
-      false
-  | _ :: tail -> aux tail
-  | [] -> false in
-  aux (List.rev trace)
-
-let explain_ltac_call_trace last trace loc =
-  let calls = last :: List.rev_map snd trace in
-  let pr_call ck = match ck with
-  | Proof_type.LtacNotationCall kn -> quote (KerName.print kn)
-  | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
-  | Proof_type.LtacMLCall t ->
-      quote (Pptactic.pr_glob_tactic (Global.env()) t)
-  | Proof_type.LtacVarCall (id,t) ->
-      quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
-        Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
-  | Proof_type.LtacAtomCall te ->
-      quote (Pptactic.pr_glob_tactic (Global.env())
-              (Tacexpr.TacAtom (Loc.ghost,te)))
-  | Proof_type.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) ->
-      quote (pr_glob_constr_env (Global.env()) c) ++
-        (if not (Id.Map.is_empty vars) then
-          strbrk " (with " ++
-            prlist_with_sep pr_comma
-            (fun (id,c) ->
-                pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
-            (List.rev (Id.Map.bindings vars)) ++ str ")"
-        else mt())
-  in
-  match calls with
-  | [] -> mt ()
-  | _ ->
-    let kind_of_last_call = match List.last calls with
-    | Proof_type.LtacConstrInterp _ -> ", last term evaluation failed."
-    | _ -> ", last call failed."
-    in
-    hov 0 (str "In nested Ltac calls to " ++
-           pr_enum pr_call calls ++ strbrk kind_of_last_call)
-
-let skip_extensions trace =
-  let rec aux = function
-  | (_,Proof_type.LtacNameCall f as tac) :: _ 
-      when Tacenv.is_ltac_for_ml_tactic f -> [tac]
-  | (_,(Proof_type.LtacNotationCall _ | Proof_type.LtacMLCall _) as tac)
-      :: _ -> [tac]
-  | t :: tail -> t :: aux tail
-  | [] -> [] in
-  List.rev (aux (List.rev trace))
-
-let extract_ltac_trace trace eloc =
-  let trace = skip_extensions trace in
-  let (loc,c),tail = List.sep_last trace in
-  if is_defined_ltac trace then
-    (* We entered a user-defined tactic,
-       we display the trace with location of the call *)
-    let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in
-    Some msg, loc
-  else
-    (* We entered a primitive tactic, we don't display trace but
-       report on the finest location *)
-    let best_loc =
-      if not (Loc.is_ghost eloc) then eloc else
-        (* trace is with innermost call coming first *)
-        let rec aux = function
-        | (loc,_)::tail when not (Loc.is_ghost loc) -> loc
-        | _::tail -> aux tail
-        | [] -> Loc.ghost in
-        aux trace in
-    None, best_loc
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 3d5442bb17..ced54fd279 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -36,9 +36,6 @@ val explain_pattern_matching_error :
 val explain_reduction_tactic_error :
   Tacred.reduction_tactic_error -> std_ppcmds
 
-val extract_ltac_trace :
-  Proof_type.ltac_trace -> Loc.t -> std_ppcmds option * Loc.t
-
 val explain_module_error : Modops.module_typing_error -> std_ppcmds
 
 val explain_module_internalization_error :
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 0d39466ede..35717ed61d 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -28,11 +28,10 @@ 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
 
@@ -114,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 =
@@ -125,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;
@@ -136,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 98eaac0928..20f30d6d16 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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 286d164c42..367425546f 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -38,6 +38,7 @@ open Ind_tables
 open Auto_ind_decl
 open Eqschemes
 open Elimschemes
+open Context.Rel.Declaration
 
 (* Flags governing automatic synthesis of schemes *)
 
@@ -128,8 +129,8 @@ let define id internal ctx c t =
       { const_entry_body = c;
         const_entry_secctx = None;
         const_entry_type = t;
-	const_entry_polymorphic = true;
-	const_entry_universes = Evd.universe_context ctx;
+	const_entry_polymorphic = Flags.is_universe_polymorphism ();
+	const_entry_universes = snd (Evd.universe_context ctx);
         const_entry_opaque = false;
         const_entry_inline_code = false;
         const_entry_feedback = None;
@@ -146,16 +147,18 @@ 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."))
-  | _ -> errorlabstrm "" msg
+	(hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None
+  | _ -> Some msg
 
 let try_declare_scheme what f internal names kn =
   try f internal names kn
-  with
+  with e ->
+  let e = Errors.push e in
+  let msg = match fst e with
     | ParameterWithoutEquality cst ->
 	alarm what internal
 	  (str "Boolean equality not found for parameter " ++ pr_con cst ++
@@ -186,6 +189,11 @@ let try_declare_scheme what f internal names kn =
     | e when Errors.noncritical e ->
         alarm what internal
 	  (str "Unexpected error during scheme creation: " ++ Errors.print e)
+    | _ -> iraise e
+  in
+  match msg with
+  | None -> ()
+  | Some msg -> iraise (UserError ("", msg), snd e)
 
 let beq_scheme_msg mind =
   let mib = Global.lookup_mind mind in
@@ -195,13 +203,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 []
 
@@ -215,7 +223,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 *)
 
@@ -238,7 +246,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 =
@@ -261,11 +269,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 []
 
@@ -274,17 +282,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 =
@@ -293,7 +301,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
@@ -301,7 +309,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 *)
 
@@ -360,19 +368,28 @@ requested
 let do_mutual_induction_scheme lnamedepindsort =
   let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
   and env0 = Global.env() in
-  let sigma, lrecspec =
+  let sigma, lrecspec, _ =
     List.fold_right
-      (fun (_,dep,ind,sort) (evd, l) -> 
-        let evd, indu = Evd.fresh_inductive_instance env0 evd ind in
-          (evd, (indu,dep,interp_elimination_sort sort) :: l))
-    lnamedepindsort (Evd.from_env env0,[])
+      (fun (_,dep,ind,sort) (evd, l, inst) -> 
+       let evd, indu, inst =
+	 match inst with
+	 | None ->
+	    let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in
+	    let ctxs = Univ.ContextSet.of_context ctx in
+	    let evd = Evd.from_ctx (Evd.evar_universe_context_of ctxs) in
+	    let u = Univ.UContext.instance ctx in
+	      evd, (ind,u), Some u
+	 | Some ui -> evd, (ind, ui), inst
+       in
+          (evd, (indu,dep,interp_elimination_sort sort) :: l, inst))
+    lnamedepindsort (Evd.from_env env0,[],None)
   in
   let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
   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
@@ -423,7 +440,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 =
@@ -454,7 +471,7 @@ let build_combined_scheme env schemes =
   in
   let ctx, _ =
     list_split_rev_at prods
-      (List.rev_map (fun (x, y) -> x, None, y) ctx) in
+      (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in
   let typ = it_mkProd_wo_LetIn concl_typ ctx in
   let body = it_mkLambda_or_LetIn concl_bod ctx in
   (body, typ)
@@ -469,8 +486,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/indschemes.mli b/toplevel/indschemes.mli
index 9874610786..e5d79fd514 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index 1145a20bbc..ef789aa5c5 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/locality.mli b/toplevel/locality.mli
index c395fe921b..2ec392eefc 100644
--- a/toplevel/locality.mli
+++ b/toplevel/locality.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 9864182a07..7c1f05cd3e 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -43,163 +43,6 @@ let inToken : string -> obj =
 let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
 (**********************************************************************)
-(* Tactic Notation                                                    *)
-
-let interp_prod_item lev = function
-  | TacTerm s -> GramTerminal s
-  | TacNonTerm (loc, nt, po) ->
-      let sep = match po with Some (_,sep) -> sep | _ -> "" in
-      let (etyp, e) = interp_entry_name true (Some lev) nt sep in
-      GramNonTerminal (loc, etyp, e, Option.map fst po)
-
-let make_terminal_status = function
-  | GramTerminal s -> Some s
-  | GramNonTerminal _ -> None
-
-let rec make_tags = function
-  | GramTerminal s :: l -> make_tags l
-  | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l
-  | [] -> []
-
-let make_fresh_key =
-  let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
-  fun () ->
-    let cur = incr id; !id in
-    let lbl = Id.of_string ("_" ^ string_of_int cur) in
-    let kn = Lib.make_kn lbl in
-    let (mp, dir, _) = KerName.repr kn in
-    (** We embed the full path of the kernel name in the label so that the
-        identifier should be unique. This ensures that including two modules
-        together won't confuse the corresponding labels. *)
-    let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i"
-      (ModPath.to_string mp) (DirPath.to_string dir) cur)
-    in
-    KerName.make mp dir (Label.of_id lbl)
-
-type tactic_grammar_obj = {
-  tacobj_key : KerName.t;
-  tacobj_local : locality_flag;
-  tacobj_tacgram : tactic_grammar;
-  tacobj_tacpp : Pptactic.pp_tactic;
-  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
-
-let open_tactic_notation i (_, tobj) =
-  let key = tobj.tacobj_key in
-  if Int.equal i 1 && not tobj.tacobj_local then
-    Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
-
-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;
-  if Int.equal i 1 && not tobj.tacobj_local then
-    Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
-
-let subst_tactic_notation (subst, tobj) =
-  { tobj with
-    tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
-    tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body;
-  }
-
-let classify_tactic_notation tacobj = Substitute tacobj
-
-let inTacticGrammar : tactic_grammar_obj -> obj =
-  declare_object {(default_object "TacticGrammar") with
-       open_function = open_tactic_notation;
-       load_function = load_tactic_notation;
-       cache_function = cache_tactic_notation;
-       subst_function = subst_tactic_notation;
-       classify_function = classify_tactic_notation}
-
-let cons_production_parameter l = function
-  | GramTerminal _ -> l
-  | GramNonTerminal (_,_,_,ido) -> Option.List.cons ido l
-
-let add_tactic_notation (local,n,prods,e) =
-  let prods = List.map (interp_prod_item n) prods in
-  let tags = make_tags prods in
-  let pprule = {
-    Pptactic.pptac_args = tags;
-    pptac_prods = (n, List.map make_terminal_status prods);
-  } in
-  let ids = List.fold_left cons_production_parameter [] prods in
-  let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
-  let parule = {
-    tacgram_level = n;
-    tacgram_prods = prods;
-  } in
-  let tacobj = {
-    tacobj_key = make_fresh_key ();
-    tacobj_local = local;
-    tacobj_tacgram = parule;
-    tacobj_tacpp = pprule;
-    tacobj_body = tac;
-  } in
-  Lib.add_anonymous_leaf (inTacticGrammar tacobj)
-
-(**********************************************************************)
-(* ML Tactic entries                                                  *)
-
-type atomic_entry = string * Genarg.glob_generic_argument list option
-
-type ml_tactic_grammar_obj = {
-  mltacobj_name : Tacexpr.ml_tactic_name;
-  (** ML-side unique name *)
-  mltacobj_prod : grammar_prod_item list list;
-  (** Grammar rules generating the ML tactic. *)
-}
-
-(** ML tactic notations whose use can be restricted to an identifier are added
-    as true Ltac entries. *)
-let extend_atomic_tactic name entries =
-  let add_atomic i (id, args) = match args with
-  | None -> ()
-  | Some args ->
-    let open Tacexpr in
-    let entry = { mltac_name = name; mltac_index = i } in
-    let body = TacML (Loc.ghost, entry, args) in
-    Tacenv.register_ltac false false (Names.Id.of_string id) body
-  in
-  List.iteri add_atomic entries
-
-let cache_ml_tactic_notation (_, obj) =
-  extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod
-
-let open_ml_tactic_notation i obj =
-  if Int.equal i 1 then cache_ml_tactic_notation obj
-
-let inMLTacticGrammar : ml_tactic_grammar_obj -> obj =
-  declare_object { (default_object "MLTacticGrammar") with
-    open_function = open_ml_tactic_notation;
-    cache_function = cache_ml_tactic_notation;
-    classify_function = (fun o -> Substitute o);
-    subst_function = (fun (_, o) -> o);
-  }
-
-let add_ml_tactic_notation name prods atomic =
-  let obj = {
-    mltacobj_name = name;
-    mltacobj_prod = prods;
-  } in
-  Lib.add_anonymous_leaf (inMLTacticGrammar obj);
-  extend_atomic_tactic name atomic
-
-(**********************************************************************)
 (* Printing grammar entries                                           *)
 
 let entry_buf = Buffer.create 64
@@ -542,10 +385,15 @@ let add_break_if_none n = function
   | l -> UnpCut (PpBrk(n,0)) :: l
 
 let check_open_binder isopen sl m =
+  let pr_token = function
+  | Terminal s -> str s
+  | Break n -> str "�"
+  | _ -> assert false
+  in
   if isopen && not (List.is_empty sl) then
     errorlabstrm "" (str "as " ++ pr_id m ++
       str " is a non-closed binder, no such \"" ++
-      prlist_with_sep spc (function Terminal s -> str s | _ -> assert false) sl
+      prlist_with_sep spc pr_token sl
       ++ strbrk "\" is allowed to occur.")
 
 (* Heuristics for building default printing rules *)
@@ -975,9 +823,10 @@ let make_internalization_vars recvars mainvars typs =
   let extratyps = List.map (fun (x,y) -> (y,List.assoc x maintyps)) recvars in
   maintyps @ extratyps
 
-let make_interpretation_type isrec = function
+let make_interpretation_type isrec isonlybinding = function
   | NtnInternTypeConstr when isrec -> NtnTypeConstrList
-  | NtnInternTypeConstr | NtnInternTypeIdent -> NtnTypeConstr
+  | NtnInternTypeConstr | NtnInternTypeIdent ->
+     if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr
   | NtnInternTypeBinder when isrec -> NtnTypeBinderList
   | NtnInternTypeBinder -> error "Type not allowed in recursive notation."
 
@@ -987,16 +836,16 @@ let make_interpretation_vars recvars allvars =
     List.equal String.equal l1 l2
   in
   let check (x, y) =
-    let (scope1, _) = Id.Map.find x allvars in
-    let (scope2, _) = Id.Map.find y allvars in
+    let (_,scope1, _) = Id.Map.find x allvars in
+    let (_,scope2, _) = Id.Map.find y allvars in
     if not (eq_subscope scope1 scope2) then error_not_same_scope x y
   in
   let () = List.iter check recvars in
   let useless_recvars = List.map snd recvars in
   let mainvars =
     Id.Map.filter (fun x _ -> not (Id.List.mem x useless_recvars)) allvars in
-  Id.Map.mapi (fun x (sc, typ) ->
-    (sc, make_interpretation_type (Id.List.mem_assoc x recvars) typ)) mainvars
+  Id.Map.mapi (fun x (isonlybinding, sc, typ) ->
+    (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars
 
 let check_rule_productivity l =
   if List.for_all (function NonTerminal _ -> true | _ -> false) l then
@@ -1450,7 +1299,7 @@ let add_syntactic_definition ident (vars,c) local onlyparse =
       } in
       let nvars, pat = interp_notation_constr nenv c in
       let () = nonprintable := nenv.ninterp_only_parse in
-      let map id = let (sc, _) = Id.Map.find id nvars in (id, sc) in
+      let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in
       List.map map vars, pat
   in
   let onlyparse = match onlyparse with
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index f22839f489..085cc87c8b 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -15,17 +15,6 @@ open Notation_term
 
 val add_token_obj : string -> unit
 
-(** Adding a tactic notation in the environment *)
-
-val add_tactic_notation :
-  locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr ->
-    unit
-
-type atomic_entry = string * Genarg.glob_generic_argument list option
-
-val add_ml_tactic_notation : ml_tactic_name ->
-  Egramml.grammar_prod_item list list -> atomic_entry list -> unit
-
 (** Adding a (constr) notation in the environment*)
 
 val add_infix : locality_flag -> (lstring * syntax_modifier list) ->
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index fa5ed7bbd7..d0fa7a80c2 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 4f3f4ddde4..5d05468241 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 738e93e2f9..b2fc456d07 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -13,7 +13,6 @@ open Declare
 *)
 
 open Term
-open Context
 open Vars
 open Names
 open Evd
@@ -44,7 +43,7 @@ let check_evars env evm =
 
 type oblinfo =
   { ev_name: int * Id.t;
-    ev_hyps: named_context;
+    ev_hyps: Context.Named.t;
     ev_status: Evar_kinds.obligation_definition_status;
     ev_chop: int option;
     ev_src: Evar_kinds.t Loc.located;
@@ -52,13 +51,11 @@ type oblinfo =
     ev_tac: unit Proofview.tactic option;
     ev_deps: Int.Set.t }
 
-(* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *)
-let evar_tactic = Store.field ()
-
 (** Substitute evar references in t using De Bruijn indices,
   where n binders were passed through. *)
 
-let subst_evar_constr evs n idf t = 
+let subst_evar_constr evs n idf t =
+  let open Context.Named.Declaration in
   let seen = ref Int.Set.empty in
   let transparent = ref Id.Set.empty in
   let evar_info id = List.assoc_f Evar.equal id evs in
@@ -82,9 +79,9 @@ let subst_evar_constr evs n idf t =
 	let args =
 	  let rec aux hyps args acc =
 	     match hyps, args with
-		 ((_, None, _) :: tlh), (c :: tla) ->
+		 (LocalAssum _ :: tlh), (c :: tla) ->
 		   aux tlh tla ((substrec (depth, fixrels) c) :: acc)
-	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
+	       | (LocalDef _ :: tlh), (_ :: tla) ->
 		   aux tlh tla acc
 	       | [], [] -> acc
 	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
@@ -120,22 +117,23 @@ let subst_vars acc n t =
     Changes evars and hypothesis references to variable references.
 *)
 let etype_of_evar evs hyps concl =
+  let open Context.Named.Declaration in
   let rec aux acc n = function
-      (id, copt, t) :: tl ->
-	let t', s, trans = subst_evar_constr evs n mkVar t in
+      decl :: tl ->
+	let t', s, trans = subst_evar_constr evs n mkVar (get_type decl) in
 	let t'' = subst_vars acc 0 t' in
-	let rest, s', trans' = aux (id :: acc) (succ n) tl in
+	let rest, s', trans' = aux (get_id decl :: acc) (succ n) tl in
 	let s' = Int.Set.union s s' in
 	let trans' = Id.Set.union trans trans' in
-	  (match copt with
-	      Some c -> 
+	  (match decl with
+            | LocalDef (id,c,_) ->
 		let c', s'', trans'' = subst_evar_constr evs n mkVar c in
 		let c' = subst_vars acc 0 c' in
-		  mkNamedProd_or_LetIn (id, Some c', t'') rest,
+		  mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
 		Int.Set.union s'' s',
 		Id.Set.union trans'' trans'
-	    | None ->
-		mkNamedProd_or_LetIn (id, None, t'') rest, s', trans')
+	    | LocalAssum (id,_) ->
+		mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
     | [] ->
 	let t', s, trans = subst_evar_constr evs n mkVar concl in
 	  subst_vars acc 0 t', s, trans
@@ -194,7 +192,7 @@ open Environ
 let eterm_obligations env name evm fs ?status t ty = 
   (* 'Serialize' the evars *)
   let nc = Environ.named_context env in
-  let nc_len = Context.named_context_length nc in
+  let nc_len = Context.Named.length nc in
   let evm = Evarutil.nf_evar_map_undefined evm in
   let evl = Evarutil.non_instantiated evm in
   let evl = Evar.Map.bindings evl in
@@ -229,17 +227,9 @@ let eterm_obligations env name evm fs ?status t ty =
 	   | Some s -> s, None
 	   | None -> Evar_kinds.Define true, None
 	 in
-	 let tac = match Store.get ev.evar_extra evar_tactic with
-	   | Some t ->
-	       if Dyn.has_tag t "tactic" then
-		 Some (Tacinterp.interp 
-			  (Tacinterp.globTacticIn (Tacinterp.tactic_out t)))
-	       else None
-	   | None -> None
-	 in
 	 let info = { ev_name = (n, nstr);
 		      ev_hyps = hyps; ev_status = status; ev_chop = chop;
-		      ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
+		      ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = None }
 	 in (id, info) :: l)
       evn []
   in
@@ -277,7 +267,7 @@ let reduce c =
 exception NoObligations of Id.t option
 
 let explain_no_obligations = function
-    Some ident -> str "No obligations for program " ++ str (Id.to_string ident)
+    Some ident -> str "No obligations for program " ++ Id.print ident
   | None -> str "No obligations remaining"
 
 type obligation_info =
@@ -311,6 +301,7 @@ type program_info_aux = {
   prg_body: constr;
   prg_type: constr;
   prg_ctx:  Evd.evar_universe_context;
+  prg_pl: Id.t Loc.located list option;
   prg_obligations: obligations;
   prg_deps : Id.t list;
   prg_fixkind : fixpoint_kind option ;
@@ -318,21 +309,21 @@ type program_info_aux = {
   prg_notations : notations ;
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
-  prg_hook : unit Lemmas.declaration_hook;
+  prg_hook : (Evd.evar_universe_context -> unit) Lemmas.declaration_hook;
   prg_opaque : bool;
+  prg_sign: named_context_val;
 }
 
-type program_info = program_info_aux Ephemeron.key
+type program_info = program_info_aux CEphemeron.key
 
 let get_info x =
-  try Ephemeron.get x
-  with Ephemeron.InvalidKey ->
+  try CEphemeron.get x
+  with CEphemeron.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) = 
-  Tactic_option.declare_tactic_option "Program tactic"
+let default_tactic = ref (Proofview.tclUNIT ())
 
 (* true = All transparent, false = Opaque if possible *)
 let proofs_transparency = ref true
@@ -459,23 +450,10 @@ let subst_deps_obl obls obl =
 
 module ProgMap = Map.Make(Id)
 
-let map_replace k v m = ProgMap.add k (Ephemeron.create v) (ProgMap.remove k m)
+let map_replace k v m = ProgMap.add k (CEphemeron.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"
 
@@ -521,16 +499,23 @@ 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 pl, ctx =
+    Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) 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;
+  let () = progmap_remove prg in
+  let cst =
     !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))
-
+     prg.prg_kind ce prg.prg_implicits
+     (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
+  in
+  Universes.register_universe_binders cst pl;
+  cst
+      
 open Pp
 
 let rec lam_index n t acc =
@@ -550,11 +535,11 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
 	 but doing it properly involves delta-reduction, and it finally
          doesn't seem to worth the effort (except for huge mutual
 	 fixpoints ?) *)
-      let m = nb_prod fixtype in
+      let m = Termops.nb_prod fixtype in
       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
@@ -594,6 +579,7 @@ let declare_mutual_definition l =
   in
   (* Declare the recursive definitions *)
   let ctx = Evd.evar_context_universe_context first.prg_ctx in
+  let fix_exn = Stm.get_fix_exn () in
   let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
     fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
@@ -601,18 +587,19 @@ let declare_mutual_definition l =
     Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
     let gr = List.hd kns in
     let kn = match gr with ConstRef kn -> kn | _ -> assert false in
-      Lemmas.call_hook (fun exn -> exn) first.prg_hook local gr;
-      List.iter progmap_remove l; kn
+    Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
+    List.iter progmap_remove l; kn
 
-let shrink_body c = 
+let shrink_body c =
+  let open Context.Rel.Declaration in
   let ctx, b = decompose_lam_assum c in
   let b', n, args = 
-    List.fold_left (fun (b, i, args) (n, u, t) ->
+    List.fold_left (fun (b, i, args) decl ->
       if noccurn 1 b then 
 	subst1 mkProp b, succ i, args
       else
-        let args = if Option.is_empty u then mkRel i :: args else args in
-        mkLambda_or_LetIn (n, u, t) b, succ i, args)
+	let args = if is_local_assum decl then mkRel i :: args else args in
+        mkLambda_or_LetIn decl b, succ i, args)
      (b, 1, []) ctx
   in ctx, b', Array.of_list args
 
@@ -625,7 +612,7 @@ 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
@@ -633,8 +620,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;
@@ -649,13 +637,14 @@ let declare_obligation prg obl body ty uctx =
       in
 	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
 	      Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
 
-let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls kind reduce hook =
+let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
+		   notations obls impls kind reduce hook =
   let obls', b = 
     match b with
     | None ->
@@ -675,12 +664,28 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls
 	  obls, b
   in
     { prg_name = n ; prg_body = b; prg_type = reduce t; 
-      prg_ctx = ctx; 
+      prg_ctx = ctx; prg_pl = pl;
       prg_obligations = (obls', Array.length obls');
       prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
       prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; 
-      prg_hook = hook;
-      prg_opaque = opaque; }
+      prg_hook = hook; prg_opaque = opaque;
+      prg_sign = sign }
+
+let map_cardinal m =
+  let i = ref 0 in
+  ProgMap.iter (fun _ v ->
+		if snd (CEphemeron.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 (CEphemeron.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
@@ -795,12 +800,12 @@ 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_terminator name num guard hook pf =
   let open Proof_global in
@@ -812,19 +817,19 @@ let obligation_terminator name num guard hook pf =
     else
       let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
       let env = Global.env () in
-      let entry = Term_typing.handle_entry_side_effects env entry in
+      let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
       let ty = entry.Entries.const_entry_type  in
       let (body, cstr), eff = Future.force entry.Entries.const_entry_body in
-      assert(Declareops.side_effects_is_empty eff);
+      assert(Safe_typing.empty_private_constants = eff);
       assert(Univ.ContextSet.is_empty cstr);
       Inductiveops.control_only_guard (Global.env ()) body;
       (** Declare the obligation ourselves and drop the hook *)
       let prg = get_info (ProgMap.find name !from_prg) in
-      let prg = { prg with prg_ctx = uctx } in
+      let prg = { prg with prg_ctx = fst uctx } in
       let obls, rem = prg.prg_obligations in
       let obl = obls.(num) in
-      let ctx = Evd.evar_context_universe_context uctx in
-      let obl = declare_obligation prg obl body ty ctx in
+      let ctx = Evd.evar_context_universe_context (fst uctx) in
+      let (_, obl) = declare_obligation prg obl body ty ctx in
       let obls = Array.copy obls in
       let _ = obls.(num) <- obl in
       try ignore (update_obls prg obls (pred rem))
@@ -847,9 +852,11 @@ let obligation_hook prg obl num auto ctx' _ gr =
   let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
   let ctx' =
     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'
+      (* The universe context was declared globally, we continue
+         from the new global environment. *)
+      let evd = Evd.from_env (Global.env ()) in
+      let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
+        Evd.evar_universe_context ctx'
     else ctx'
   in
   let prg = { prg with prg_ctx = ctx' } in
@@ -879,14 +886,15 @@ let rec solve_obligation prg num tac =
   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_env ~ctx:prg.prg_ctx Environ.empty_env in
+  let evd = Evd.from_ctx prg.prg_ctx in
+  let evd = Evd.update_sigma_env evd (Global.env ()) in
   let auto n tac oblset = auto_solve_obligations n ~oblset tac in
   let terminator guard hook = Proof_global.make_terminator (obligation_terminator prg.prg_name num guard hook) 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 ~terminator hook in
+  let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator 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
+  let _ = Pfedit.by !default_tactic in
   Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
 
 and obligation (user_num, name, typ) tac =
@@ -915,15 +923,24 @@ and solve_obligation_by_tac prg obls i tac =
 	      | None ->
 		  match obl.obl_tac with
 		  | Some t -> t
-		  | None -> snd (get_default_tactic ())
+		  | None -> !default_tactic
 	    in
+	    let evd = Evd.from_ctx !prg.prg_ctx in
+	    let evd = Evd.update_sigma_env evd (Global.env ()) in
 	    let t, ty, ctx = 
 	      solve_by_tac obl.obl_name (evar_of_obligation obl) tac 
-	        (pi2 !prg.prg_kind) !prg.prg_ctx
+	        (pi2 !prg.prg_kind) (Evd.evar_universe_context evd)
 	    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 evd = Evd.from_env (Global.env ()) in
+	        let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in
+		let ctx' = Evd.evar_universe_context evd in
+		  prg := {!prg with prg_ctx = ctx'});
 	      true
 	  else false
 	with e when Errors.noncritical e ->
@@ -988,7 +1005,7 @@ let show_obligations_of_prg ?(msg=true) prg =
 		       if !showed > 0 then (
 			 decr showed;
 			 msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
-				   str "of" ++ spc() ++ str (Id.to_string n) ++ str ":" ++ spc () ++
+				   str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
 				   hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++
 					    str "." ++ fnl ())))
 		   | Some _ -> ())
@@ -1005,14 +1022,15 @@ let show_obligations ?(msg=true) n =
 let show_term n =
   let prg = get_prog_err n in
   let n = prg.prg_name in
-    (str (Id.to_string n) ++ spc () ++ str":" ++ spc () ++
+    (Id.print n ++ spc () ++ str":" ++ spc () ++
 	     Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
 
-let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
-    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) obls =
-  let info = str (Id.to_string n) ++ str " has type-checked" in
-  let prg = init_prog_info ~opaque n term t ctx [] None [] obls implicits kind reduce hook in
+let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
+  let sign = Decls.initialize_named_context_for_proof () in
+  let info = Id.print n ++ str " has type-checked" in
+  let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose msg_info (info ++ str ".");
@@ -1021,20 +1039,21 @@ 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 (Ephemeron.create prg);
+      progmap_add n (CEphemeron.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
 	| _ -> res)
 
-let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
-    ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) notations fixkind =
+let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
+    ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
+  let sign = Decls.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
-     let prg = init_prog_info ~opaque n (Some b) t ctx deps (Some fixkind)
+     let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind)
        notations obls imps kind reduce hook 
-     in progmap_add n (Ephemeron.create prg)) l;
+     in progmap_add n (CEphemeron.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 40f124ca36..3e99f5760b 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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
@@ -54,21 +54,20 @@ type progress = (* Resolution status of a program *)
   | Remain of int  (* n obligations remaining *)
   | Dependent (* Dependent on other definitions *)
   | Defined of global_reference (* Defined as id *)
-      
-val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit
-val get_default_tactic : unit -> locality_flag * unit Proofview.tactic
-val print_default_tactic : unit -> Pp.std_ppcmds
+
+val default_tactic : unit Proofview.tactic ref
 
 val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
 val get_proofs_transparency : unit -> bool
 
 val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> 
   Evd.evar_universe_context ->
+  ?pl:(Id.t Loc.located list) -> (* Universe binders *)
   ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:unit Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
+  ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
 
 type notations =
     (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -81,10 +80,11 @@ val add_mutual_definitions :
   (Names.Id.t * Term.constr * Term.types *
       (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
   Evd.evar_universe_context ->
+  ?pl:(Id.t Loc.located list) -> (* Universe binders *)
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:unit Lemmas.declaration_hook -> ?opaque:bool ->
+  ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool ->
   notations ->
   fixpoint_kind -> unit
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 15ad18d9cc..93429da5ac 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -13,7 +13,6 @@ open Names
 open Globnames
 open Nameops
 open Term
-open Context
 open Vars
 open Environ
 open Declarations
@@ -25,6 +24,9 @@ open Type_errors
 open Constrexpr
 open Constrexpr_ops
 open Goptions
+open Sigma.Notations
+open Context.Rel.Declaration
+open Entries
 
 (********** definition d'un record (structure) **************)
 
@@ -69,16 +71,19 @@ let interp_fields_evars env evars impls_env nots l =
 	| Anonymous -> impls
 	| Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method t' impl) impls
       in
-      let d = (i,b',t') in
+      let d = match b' with
+	      | None -> LocalAssum (i,t')
+	      | Some b' -> LocalDef (i,b',t')
+      in
       List.iter (Metasyntax.set_notation_for_interpretation impls) no;
       (push_rel d env, impl :: uimpls, d::params, impls))
     (env, [], [], impls_env) nots l
 
 let compute_constructor_level evars env l =
-  List.fold_right (fun (n,b,t as d) (env, univ) ->
+  List.fold_right (fun d (env, univ) ->
     let univ = 
-      if b = None then 
-	let s = Retyping.get_sort_of env evars t in
+      if is_local_assum d then
+	let s = Retyping.get_sort_of env evars (get_type d) in
 	  Univ.sup (univ_of_sort s) univ 
       else univ
     in (push_rel d env, univ)) 
@@ -90,9 +95,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
@@ -113,16 +119,16 @@ let typecheck_params_and_fields def id t ps nots fs =
 	 (match kind_of_term sred with
 	 | Sort s' -> 
 	   (match Evd.is_sort_variable !evars s' with
-	   | Some l -> evars := Evd.make_flexible_variable !evars true (* (not def) *) l; 
+	   | Some l -> evars := Evd.make_flexible_variable !evars true l; 
 	     sred, true
 	   | None -> s, false)
 	 | _ -> user_err_loc (constr_loc t,"", str"Sort expected."))
     | None -> 
-      let uvarkind = if (* not def *) true then Evd.univ_flexible_alg else Evd.univ_flexible in
-	mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), false
+      let uvarkind = Evd.univ_flexible_alg in
+	mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true
   in
   let fullarity = it_mkProd_or_LetIn t' newps in
-  let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
+  let env_ar = push_rel_context newps (push_rel (LocalAssum (Name id,fullarity)) env0) in
   let env2,impls,newfs,data =
     interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs)
   in
@@ -130,30 +136,38 @@ 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 && is_impredicative_set env0) then
-	evars
-      else Evd.set_leq_sort env_ar evars (Type univ) aritysort
+      if not def && (Sorts.is_prop 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 &&
+	   Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars aritysort) then
+	   (* We can assume that the level in aritysort is not constrained
+	       and clear it, if it is flexible *)
+	  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
-  let newfs = map_rel_context nf newfs in
-  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
+  let newps = Context.Rel.map nf newps in
+  let newfs = Context.Rel.map nf newfs in
+  let ce t = Pretyping.check_evars env0 Evd.empty evars t in
+    List.iter (iter_constr ce) (List.rev newps);
+    List.iter (iter_constr ce) (List.rev 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
+let degenerate_decl decl =
+  let id = match get_name decl 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)
+  match decl with
+    | LocalAssum (_,t) -> (id, LocalAssumEntry t)
+    | LocalDef (_,b,_) -> (id, LocalDefEntry b)
 
 type record_error =
   | MissingProj of Id.t * Id.t list
@@ -163,7 +177,7 @@ let warning_or_error coe indsp err =
   let st = match err with
     | MissingProj (fi,projs) ->
 	let s,have = if List.length projs > 1 then "s","were" else "","was" in
-        (str(Id.to_string fi) ++
+        (pr_id fi ++
 	   strbrk" cannot be defined because the projection" ++ str s ++ spc () ++
            prlist_with_sep pr_comma pr_id projs ++ spc () ++ str have ++
 	   strbrk " not defined.")
@@ -232,11 +246,12 @@ 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
-  let paramargs = Termops.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
+  let rp = applist (r, Context.Rel.to_extended_list 0 paramdecls) in
+  let paramargs = Context.Rel.to_extended_list 1 paramdecls in (*def in [[params;x:rp]]*)
   let x = Name binder_name in
   let fields = instantiate_possibly_recursive_type indu paramdecls fields in
   let lifted_fields = Termops.lift_rel_context 1 fields in
@@ -256,23 +271,25 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
   in
   let (_,_,kinds,sp_projs,_) =
     List.fold_left3
-      (fun (nfi,i,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
+      (fun (nfi,i,kinds,sp_projs,subst) coe decl impls ->
+        let fi = get_name decl in
+        let ti = get_type decl in
 	let (sp_projs,i,subst) =
 	  match fi with
 	  | Anonymous ->
 	      (None::sp_projs,i,NoProjection fi::subst)
 	  | Name fid -> try
 	    let kn, term = 
-	      if optci = None && primitive then 
+	      if is_local_assum decl && primitive then
 		(** Already defined in the kernel silently *)
 		let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in
 		  Declare.definition_message fid;
 		  kn, mkProj (Projection.make kn false,mkRel 1)
 	      else
 		let ccl = subst_projection fid subst ti in
-		let body = match optci with
-		  | Some ci -> subst_projection fid subst ci
-		  | None ->
+		let body = match decl with
+		  | LocalDef (_,ci,_) -> subst_projection fid subst ci
+		  | LocalAssum _ ->
 	            (* [ccl] is defined in context [params;x:rp] *)
 		    (* [ccl'] is defined in context [params;x:rp;x:rp] *)
 		    let ccl' = liftn 1 2 ccl in
@@ -288,16 +305,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) 
@@ -313,28 +331,32 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 	      let cl = Class.class_of_global (IndRef indsp) in
 	        Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl
 	    end;
-	    let i = if Option.is_empty optci then i+1 else i in
+	    let i = if is_local_assum decl then i+1 else i in
 	      (Some kn::sp_projs, i, Projection term::subst)
             with NotDefinable why ->
 	      warning_or_error coe indsp why;
 	      (None::sp_projs,i,NoProjection fi::subst) in
-      (nfi-1,i,(fi, Option.is_empty optci)::kinds,sp_projs,subst))
+      (nfi-1,i,(fi, is_local_assum decl)::kinds,sp_projs,subst))
       (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
 let structure_signature ctx =
   let rec deps_to_evar evm l =
     match l with [] -> Evd.empty
-      | [(_,_,typ)] ->
+      | [decl] ->
         let env = Environ.empty_named_context_val in
-        let (evm, _) = Evarutil.new_pure_evar env evm typ in
+        let evm = Sigma.Unsafe.of_evar_map evm in
+        let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in
+        let evm = Sigma.to_evar_map evm in
         evm
-      | (_,_,typ)::tl ->
+      | decl::tl ->
           let env = Environ.empty_named_context_val in
-          let (evm, ev) = Evarutil.new_pure_evar env evm typ in
+          let evm = Sigma.Unsafe.of_evar_map evm in
+          let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in
+          let evm = Sigma.to_evar_map evm in
 	  let new_tl = Util.List.map_i
-	    (fun pos (n,c,t) -> n,c,
-	       Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) 1 tl in
+	    (fun pos decl ->
+	       map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in
 	  deps_to_evar evm new_tl in
   deps_to_evar Evd.empty (List.rev ctx)
 
@@ -343,7 +365,7 @@ open Typeclasses
 let declare_structure finite poly ctx id idbuild paramimpls params arity template 
     fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
   let nparams = List.length params and nfields = List.length fields in
-  let args = Termops.extended_rel_list nfields params in
+  let args = Context.Rel.to_extended_list nfields params in
   let ind = applist (mkRel (1+nparams+nfields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
   let binder_name = 
@@ -366,7 +388,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
@@ -382,7 +404,7 @@ let implicits_of_context ctx =
       | Name n -> Some n
       | Anonymous -> None
     in ExplByPos (i, explname), (true, true, true))
-    1 (List.rev (Anonymous :: (List.map pi1 ctx)))
+    1 (List.rev (Anonymous :: (List.map get_name ctx)))
 
 let declare_class finite def poly ctx id idbuild paramimpls params arity 
     template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
@@ -395,49 +417,54 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
   let binder_name = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
   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]
+    | [LocalAssum (Name proj_name, field) | LocalDef (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:(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 decl b y -> get_name decl, b, y)
+         (List.rev fields) coers (Recordops.lookup_projections ind)
+       in IndRef ind, l
   in
   let ctx_context =
-    List.map (fun (na, b, t) ->
-      match Typeclasses.class_of_constr t with
+    List.map (fun decl ->
+      match Typeclasses.class_of_constr (get_type decl) with
       | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true)
       | None -> None)
       params, params
@@ -459,7 +486,7 @@ let add_constant_class cst =
   let tc = 
     { cl_impl = ConstRef cst;
       cl_context = (List.map (const None) ctx, ctx);
-      cl_props = [(Anonymous, None, arity)];
+      cl_props = [LocalAssum (Anonymous, arity)];
       cl_projs = [];
       cl_strict = !typeclasses_strict;
       cl_unique = !typeclasses_unique
@@ -473,8 +500,8 @@ let add_inductive_class ind =
     let ctx = oneind.mind_arity_ctxt in
     let inst = Univ.UContext.instance mind.mind_universes in
     let map = function
-    | (_, Some _, _) -> None
-    | (_, None, t) -> Some (lazy t)
+    | LocalDef _ -> None
+    | LocalAssum (_, t) -> Some (lazy t)
     in
     let args = List.map_filter map ctx in
     let ty = Inductive.type_of_inductive_knowing_parameters
@@ -484,7 +511,7 @@ let add_inductive_class ind =
     in
       { cl_impl = IndRef ind;
 	cl_context = List.map (const None) ctx, ctx;
-	cl_props = [Anonymous, None, ty];
+	cl_props = [LocalAssum (Anonymous, ty)];
 	cl_projs = [];
 	cl_strict = !typeclasses_strict;
 	cl_unique = !typeclasses_unique }
@@ -502,7 +529,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 +544,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 +561,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 91dccb96e1..26eb3378bb 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Vernacexpr
 open Constrexpr
 open Impargs
@@ -22,15 +21,15 @@ val primitive_flag : bool ref
 
 val declare_projections :
   inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t ->
-  coercion_flag list -> manual_explicitation list list -> rel_context ->
+  coercion_flag list -> manual_explicitation list list -> Context.Rel.t ->
   (Name.t * bool) list * constant option list
 
 val declare_structure : Decl_kinds.recursivity_kind ->
   bool (** polymorphic?*) -> Univ.universe_context ->
   Id.t -> Id.t ->
-  manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *)
+  manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
   bool (** template arity ? *) ->
-  Impargs.manual_explicitation list list -> rel_context -> (** fields *)
+  Impargs.manual_explicitation list list -> Context.Rel.t -> (** fields *)
   ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
   bool -> (** coercion? *)
   bool list -> (** field coercions *)
@@ -38,7 +37,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 9c32bddad4..646e2e08ac 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -67,7 +67,9 @@ let iter_constructors indsp u fn env nconstr =
     fn (ConstructRef (indsp, i)) env typ
   done
 
-let iter_named_context_name_type f = List.iter (fun (nme,_,typ) -> f nme typ) 
+let iter_named_context_name_type f =
+  let open Context.Named.Declaration in
+  List.iter (fun decl -> f (get_id decl) (get_type decl))
 
 (* General search over hypothesis of a goal *)
 let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
@@ -79,12 +81,13 @@ let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
 
 (* General search over declarations *)
 let iter_declarations (fn : global_reference -> env -> constr -> unit) =
+  let open Context.Named.Declaration in
   let env = Global.env () in
   let iter_obj (sp, kn) lobj = match object_tag lobj with
   | "VARIABLE" ->
     begin try
-      let (id, _, typ) = Global.lookup_named (basename sp) in
-      fn (VarRef id) env typ
+      let decl = Global.lookup_named (basename sp) in
+      fn (VarRef (get_id decl)) env (get_type decl)
     with Not_found -> (* we are in a section *) () end
   | "CONSTANT" ->
     let cst = Global.constant_of_delta_kn kn in
diff --git a/toplevel/search.mli b/toplevel/search.mli
index f69489c3d2..78b0c45c01 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 1144ffb940..f855c096e3 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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\
@@ -73,6 +73,9 @@ let print_usage_channel co command =
 \n  -impredicative-set     set sort Set impredicative\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
+\n  -xml                   export XML files either to the hierarchy rooted in\
+\n                         the directory $COQ_XML_LIBRARY_ROOT (if set) or to\
+\n                         stdout (if unset)\
 \n  -time                  display the time taken by each command\
 \n  -m, --memory           display total heap size at program exit\
 \n                         (use environment variable\
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index ed0cd477c7..3ce9e93ee5 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 266d8f9b4f..89bc31d0ac 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -27,9 +27,9 @@ let rec is_navigation_vernac = function
   | VernacBacktrack _
   | VernacBackTo _
   | VernacBack _ -> true
-  | VernacRedirect (_, l) | VernacTime l ->
-    List.exists
-      (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *)
+  | VernacRedirect (_, (_,c))
+  | VernacTime (_,c) ->
+      is_navigation_vernac c (* Time Back* is harmless *)
   | c -> is_deep_navigation_vernac c
 
 and is_deep_navigation_vernac = function
@@ -97,10 +97,7 @@ let user_error loc s = Errors.user_err_loc (loc,"_",str s)
    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
@@ -153,7 +150,6 @@ let pr_new_syntax loc ocom =
   if !beautify_file then set_formatter_translator();
   let fs = States.freeze ~marshallable:`No in
   let com = match ocom with
-    | Some VernacNop -> mt()
     | Some com -> Ppvernac.pr_vernac com
     | None -> mt() in
   if !beautify_file then
@@ -206,19 +202,17 @@ 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
@@ -234,7 +228,7 @@ let rec vernac_com verbose checknav (loc,com) =
       checknav loc com;
       if do_beautify () then pr_new_syntax loc (Some com);
       if !Flags.time then display_cmd_header loc com;
-      let com = if !Flags.time then VernacTime [loc,com] else com in
+      let com = if !Flags.time then VernacTime (loc,com) else com in
       interp com
     with reraise ->
       let (reraise, info) = Errors.push reraise in
@@ -282,6 +276,10 @@ let checknav loc ast =
 
 let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
 
+(* XML output hooks *)
+let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
+let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore ()
+
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =
   chan_beautify :=
@@ -294,7 +292,15 @@ let load_vernac verb file =
     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
@@ -302,11 +308,13 @@ 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;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
+      if !Flags.xml_export then Hook.get f_xml_start_library ();
       let wall_clock1 = Unix.gettimeofday () in
       let _ = load_vernac verbosely long_f_dot_v in
       Stm.join ();
@@ -316,9 +324,11 @@ let compile verbosely f =
       Aux_file.record_in_aux_at Loc.ghost "vo_compile_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       Aux_file.stop_aux_file ();
+      if !Flags.xml_export then Hook.get f_xml_end_library ();
       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
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index affc21713d..008d7a31aa 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -23,6 +23,10 @@ val just_parsing : bool ref
 
 val eval_expr : Loc.t * Vernacexpr.vernac_expr -> unit
 
+(** Set XML hooks *)
+val xml_start_library : (unit -> unit) Hook.t
+val xml_end_library   : (unit -> unit) Hook.t
+
 (** Load a vernac file, verbosely or not. Errors are annotated with file
    and location *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index cfbdaccec4..12869e3d57 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -20,7 +20,6 @@ open Tacmach
 open Constrintern
 open Prettyp
 open Printer
-open Tacinterp
 open Command
 open Goptions
 open Libnames
@@ -32,6 +31,10 @@ open Redexpr
 open Lemmas
 open Misctypes
 open Locality
+open Sigma.Notations
+
+(** TODO: make this function independent of Ltac *)
+let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
 
 let debug = false
 let prerr_endline =
@@ -45,7 +48,7 @@ let cl_of_qualid = function
   | RefClass r -> Class.class_of_global (Smartlocate.smart_global ~head:true r)
 
 let scope_class_of_qualid qid =
-  Notation.scope_class_of_reference (Smartlocate.smart_global qid)
+  Notation.scope_class_of_class (cl_of_qualid qid)
 
 (*******************)
 (* "Show" commands *)
@@ -76,9 +79,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 *)
@@ -157,7 +159,7 @@ let show_match id =
 (* "Print" commands *)
 
 let print_path_entry p =
-  let dir = str (DirPath.to_string (Loadpath.logical p)) in
+  let dir = pr_dirpath (Loadpath.logical p) in
   let path = str (Loadpath.physical p) in
   (dir ++ str " " ++ tbrk (0, 0) ++ path)
 
@@ -334,7 +336,7 @@ let dump_universes_gen g s =
           | Univ.Eq ->
             Printf.fprintf output "  \"%s\" -> \"%s\" [style=dashed];\n" left right
       end, begin fun () ->
-        if Lazy.lazy_is_val init then Printf.fprintf output "}\n";
+        if Lazy.is_val init then Printf.fprintf output "}\n";
         close_out output
       end
     end else begin
@@ -348,7 +350,7 @@ let dump_universes_gen g s =
     end
   in
   try
-    Univ.dump_universes output_constraint g;
+    UGraph.dump_universes output_constraint g;
     close ();
     msg_info (str "Universes written to file \"" ++ str s ++ str "\".")
   with reraise ->
@@ -356,17 +358,11 @@ let dump_universes_gen g s =
     close ();
     iraise reraise
 
-let dump_universes sorted s =
-  let g = Global.universes () in
-  let g = if sorted then Univ.sort_universes g else g in
-  dump_universes_gen g 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
@@ -461,7 +457,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
@@ -471,26 +467,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)
+ 		Some (snd (Hook.get f_interp_redexp env evc r)) in
+	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
 
@@ -517,7 +514,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
@@ -525,11 +522,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"
@@ -538,7 +535,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";
@@ -553,12 +550,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"
@@ -578,13 +575,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 =
@@ -603,8 +600,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            *)
@@ -820,35 +828,6 @@ let vernac_declare_class id =
 let command_focus = Proof.new_focus_kind ()
 let focus_command_cond = Proof.no_cond command_focus
 
-
-let print_info_trace = ref None
-
-let _ = let open Goptions in declare_int_option {
-  optsync = true;
-  optdepr = false;
-  optname = "print info trace";
-  optkey = ["Info" ; "Level"];
-  optread = (fun () -> !print_info_trace);
-  optwrite = fun n -> print_info_trace := n;
-}
-
-let vernac_solve n info tcom b =
-  if not (refining ()) then
-    error "Unknown command of the non proof-editing mode.";
-  let status = Proof_global.with_current_proof (fun etac p ->
-    let with_end_tac = if b then Some etac else None in
-    let global = match n with SelectAll -> true | _ -> false in
-    let info = Option.append info !print_info_trace in
-    let (p,status) =
-      solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
-    in
-    (* in case a strict subtree was completed,
-       go back to the top of the prooftree *)
-    let p = Proof.maximal_unfocus command_focus p in
-    p,status) in
-    if not status then Pp.feedback Feedback.AddedAxiom
- 
-
   (* A command which should be a tactic. It has been
      added by Christine to patch an error in the design of the proof
      machine, and enables to instantiate existential variables when
@@ -866,31 +845,25 @@ let vernac_set_end_tac tac =
     (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
 
 let vernac_set_used_variables e =
+  let open Context.Named.Declaration in
   let env = Global.env () in
   let tys =
     List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in
   let l = Proof_using.process_expr env e tys in
   let vars = Environ.named_context env in
   List.iter (fun id -> 
-    if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then
+    if not (List.exists (Id.equal id % get_id) vars) then
       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
-  vernac_solve
-    SelectAll None Tacexpr.(TacAtom (Loc.ghost,TacClear(false,to_clear))) false
-
+  let _, to_clear = set_used_variables l in
+  let to_clear = List.map snd to_clear in
+  Proof_global.with_current_proof begin fun _ p ->
+    if List.is_empty to_clear then (p, ())
+    else
+      let tac = Proofview.V82.tactic (Tactics.clear to_clear) in
+      fst (solve SelectAll None tac p), ()
+  end
 
 (*****************************)
 (* Auxiliary file management *)
@@ -930,94 +903,17 @@ 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
 
 (************)
 (* Commands *)
 
-type tacdef_kind =
-  | NewTac of Id.t
-  | UpdateTac of Nametab.ltac_constant
-
-let is_defined_tac kn =
-  try ignore (Tacenv.interp_ltac kn); true with Not_found -> false
-
-let make_absolute_name ident repl =
-  let loc = loc_of_reference ident in
-  if repl then
-    let kn =
-      try Nametab.locate_tactic (snd (qualid_of_reference ident))
-      with Not_found ->
-        Errors.user_err_loc (loc, "",
-                    str "There is no Ltac named " ++ pr_reference ident ++ str ".")
-    in
-    UpdateTac kn
-  else
-    let id = Constrexpr_ops.coerce_reference_to_id ident in
-    let kn = Lib.make_kn id in
-    let () = if is_defined_tac kn then
-      Errors.user_err_loc (loc, "",
-        str "There is already an Ltac named " ++ pr_reference ident ++ str".")
-    in
-    let is_primitive =
-      try
-        match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with
-        | Tacexpr.TacArg _ -> false
-        | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
-      with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
-    in
-    let () = if is_primitive then
-      msg_warning (str "The Ltac name " ++ pr_reference ident ++
-        str " may be unusable because of a conflict with a notation.")
-    in
-    NewTac id
-
-let register_ltac local isrec tacl =
-  let map (ident, repl, body) =
-    let name = make_absolute_name ident repl in
-    (name, body)
-  in
-  let rfun = List.map map tacl in
-  let recvars =
-    let fold accu (op, _) = match op with
-    | UpdateTac _ -> accu
-    | NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu
-    in
-    if isrec then List.fold_left fold [] rfun
-    else []
-  in
-  let ist = Tacintern.make_empty_glob_sign () in
-  let map (name, body) =
-    let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in
-    (name, body)
-  in
-  let defs () =
-    (** Register locally the tactic to handle recursivity. This function affects
-        the whole environment, so that we transactify it afterwards. *)
-    let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in
-    let () = List.iter iter_rec recvars in
-    List.map map rfun
-  in
-  let defs = Future.transactify defs () in
-  let iter (def, tac) = match def with
-  | NewTac id ->
-    Tacenv.register_ltac false local id tac;
-    Flags.if_verbose msg_info (Nameops.pr_id id ++ str " is defined")
-  | UpdateTac kn ->
-    Tacenv.redefine_ltac local kn tac;
-    let name = Nametab.shortest_qualid_of_tactic kn in
-    Flags.if_verbose msg_info (Libnames.pr_qualid name ++ str " is redefined")
-  in
-  List.iter iter defs
-
-let vernac_declare_tactic_definition locality (x,def) =
-  let local = make_module_locality locality in
-  register_ltac local x def
-
 let vernac_create_hintdb locality id b =
   let local = make_module_locality locality in
   Hints.create_hint_db local id full_transparent_state b
@@ -1184,8 +1080,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
@@ -1357,19 +1254,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 ->
@@ -1385,15 +1273,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) *)
 
@@ -1451,18 +1330,6 @@ let _ =
       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)
-
-let _ =
-  declare_bool_option
-    { optsync  = false;
-      optdepr  = false;
-      optname  = "Ltac debug";
-      optkey   = ["Ltac";"Debug"];
-      optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
-      optwrite = vernac_debug }
-
 let _ =
   declare_bool_option
     { optsync  = true;
@@ -1496,6 +1363,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
 
@@ -1541,7 +1410,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 =
@@ -1556,16 +1425,20 @@ 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
-	let redfun env evm c = snd (fst (reduction_of_red_expr env r_interp) env evm c) in
+        let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in
+	let redfun env evm c =
+          let (redfun, _) = reduction_of_red_expr env r_interp in
+          let evm = Sigma.Unsafe.of_evar_map evm in
+          let Sigma (c, _, _) = redfun.Reductionops.e_redfun env evm c in
+          c
+        in
 	msg_notice (print_eval redfun env sigma' rc j)
 
 let vernac_declare_reduction locality s r =
   let local = make_locality locality in
-  declare_red_expr local s (snd (interp_redexp (Global.env()) Evd.empty r))
+  declare_red_expr local s (snd (Hook.get f_interp_redexp (Global.env()) Evd.empty r))
 
   (* The same but avoiding the current goal context if any *)
 let vernac_global_check c =
@@ -1573,7 +1446,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 Univ.UContext.empty ctx) in
+  let cstrs = snd (UState.context_set 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
@@ -1591,6 +1464,7 @@ exception NoHyp
    We only print the type and a small statement to this comes from the
    goal. Precondition: there must be at least one current goal. *)
 let print_about_hyp_globs ref_or_by_not glnumopt =
+  let open Context.Named.Declaration in
   try
     let gl,id =
       match glnumopt,ref_or_by_not with
@@ -1603,11 +1477,11 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
                            (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
-    let natureofid = match bdyopt with
-      | None -> "Hypothesis"
-      | Some bdy ->"Constant (let in)" in
-    v 0 (str (Id.to_string id) ++ str":" ++ pr_constr typ ++ fnl() ++ fnl()
+    let decl = Context.Named.lookup id hyps in
+    let natureofid = match decl with
+                     | LocalAssum _ -> "Hypothesis"
+                     | LocalDef (_,bdy,_) ->"Constant (let in)" in
+    v 0 (pr_id id ++ str":" ++ pr_constr (get_type decl) ++ fnl() ++ fnl()
 	 ++ str natureofid ++ str " of the goal context.")
   with (* fallback to globals *)
     | NoHyp | Not_found -> print_about ref_or_by_not
@@ -1632,24 +1506,24 @@ let vernac_print = function
   | PrintClasses -> msg_notice (Prettyp.print_classes())
   | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
   | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c))
-  | PrintLtac qid -> msg_notice (Tacintern.print_ltac (snd (qualid_of_reference qid)))
   | PrintCoercions -> msg_notice (Prettyp.print_coercions())
   | PrintCoercionPaths (cls,clt) ->
       msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
   | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ())
-  | PrintUniverses (b, None) ->
+  | PrintUniverses (b, dst) ->
      let univ = Global.universes () in
-     let univ = if b then Univ.sort_universes univ else univ in
+     let univ = if b then UGraph.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
+     begin match dst with
+     | None -> msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
+     | Some s -> dump_universes_gen univ s
+     end
   | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
   | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())
   | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s)
-  | PrintRewriteHintDbName s -> msg_notice (Autorewrite.print_rewrite_hintdb s)
   | PrintHintDb -> msg_notice (Hints.pr_searchtable ())
   | PrintScopes ->
       msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr))
@@ -1800,6 +1674,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 ->
@@ -1845,9 +1720,7 @@ let vernac_load interp 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
@@ -1856,8 +1729,9 @@ 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 *)
@@ -1871,8 +1745,6 @@ let interp ?proof locality poly c =
   | VernacError e -> raise e
 
   (* Syntax *)
-  | VernacTacticNotation (n,r,e) ->
-      Metasyntax.add_tactic_notation (make_module_locality locality,n,r,e)
   | VernacSyntaxExtension (local,sl) ->
       vernac_syntax_extension locality local sl
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
@@ -1887,7 +1759,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
@@ -1896,8 +1768,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) ->
@@ -1930,7 +1802,6 @@ let interp ?proof locality poly c =
   | VernacDeclareClass id -> vernac_declare_class id
 
   (* Solving *)
-  | VernacSolve (n,info,tac,b) -> vernac_solve n info tac b
   | VernacSolveExistential (n,c) -> vernac_solve_existential n c
 
   (* Auxiliary file and library management *)
@@ -1951,8 +1822,6 @@ let interp ?proof locality poly c =
   | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm")
 
   (* Commands *)
-  | VernacDeclareTacticDefinition def ->
-      vernac_declare_tactic_definition locality def
   | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b
   | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids
   | VernacHints (local,dbnames,hints) ->
@@ -1981,7 +1850,6 @@ let interp ?proof locality poly c =
   | VernacLocate l -> vernac_locate l
   | VernacRegister (id, r) -> vernac_register id r
   | VernacComments l -> if_verbose msg_info (str "Comments ok\n")
-  | VernacNop -> ()
 
   (* The STM should handle that, but LOAD bypasses the STM... *)
   | VernacAbort id -> msg_warning (str "VernacAbort not handled by Stm")
@@ -1992,7 +1860,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 ()
@@ -2001,10 +1869,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 *)
@@ -2023,15 +1897,13 @@ let check_vernac_supports_locality c l =
   match l, c with
   | None, _ -> ()
   | Some _, (
-      VernacTacticNotation _
-    | VernacOpenCloseScope _
+      VernacOpenCloseScope _
     | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
     | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
-    | VernacAssumption _
+    | VernacAssumption _ | VernacStartTheoremProof _
     | VernacCoercion _ | VernacIdentityCoercion _
     | VernacInstance _ | VernacDeclareInstances _
     | VernacDeclareMLModule _
-    | VernacDeclareTacticDefinition _
     | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
     | VernacSyntacticDefinition _
     | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _
@@ -2054,12 +1926,12 @@ 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
   | None -> Flags.is_universe_polymorphism ()
-  | Some b -> b
+  | Some b -> Flags.make_polymorphic_flag b; b
 
 (** A global default timeout, controled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
@@ -2143,11 +2015,11 @@ 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 ->
+    | VernacRedirect (s, (_,v)) ->
+         Pp.with_output_to_file s (aux false) v
+    | VernacTime (_,v) ->
         System.with_time !Flags.time
-          (aux_list ?locality ?polymorphism isprogcmd) v;
+          (aux ?locality ?polymorphism isprogcmd) v;
     | VernacLoad (_,fname) -> vernac_load (aux false) fname
     | c -> 
         check_vernac_supports_locality c locality;
@@ -2156,10 +2028,12 @@ 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
+            Flags.program_mode := orig_program_mode;
+	  ignore (Flags.use_polymorphic_flag ())
           end
         with
         | reraise when
@@ -2171,9 +2045,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
             let e = locate_if_not_already loc e in
             let () = restore_timeout () in
             Flags.program_mode := orig_program_mode;
+	    ignore (Flags.use_polymorphic_flag ());
             iraise e
-  and aux_list ?locality ?polymorphism isprogcmd l =
-    List.iter (aux false) (List.map snd l)
   in
     if verbosely then Flags.verbosely (aux false) c
     else aux false c
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 4b1cd7a013..4e7fa4a087 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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
@@ -56,3 +59,8 @@ val vernac_end_proof :
   ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
 
 val with_fail : bool -> (unit -> unit) -> unit
+
+val command_focus : unit Proof.focus_kind
+
+val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Tacexpr.raw_red_expr ->
+  Evd.evar_map * Redexpr.red_expr) Hook.t
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index d3e48f756e..7fbd2b1196 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 0282065469..5149b5416d 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)