25 files changed, 248 insertions, 162 deletions
diff --git a/CHANGES b/CHANGES
index a270aef96d..68cc495f58 100644
--- a/CHANGES
+++ b/CHANGES
@@ -19,6 +19,12 @@ Vernacular Commands
 - Removed deprecated commands Arguments Scope and Implicit Arguments
   (not the option). Use the Arguments command instead.
 
+Tactics
+
+- Introduction tactics "intro"/"intros" on a goal which is an
+  existential variable now force a refinement of the goal into a
+  dependent product rather than failing.
+
 Tactic language
 
 - Support for fix/cofix added in Ltac "match" and "lazymatch".
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index a3d06ae046..6c1b1c08c1 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -634,7 +634,12 @@ puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or
 ``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the
 new subgoal is :g:`U`.
 
-If the goal is neither a product nor starting with a let definition,
+If the goal is an existential variable, ``intro`` forces the resolution of the
+existential variable into a dependent product :math:`\forall`:g:`x:?X, ?Y`, puts
+:g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal allowed to
+depend on :g:`x`.
+
+If the goal is neither a product, nor starting with a let definition, nor an existential variable,
 the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can
 be applied or the goal is not head-reducible.
 
diff --git a/engine/evd.ml b/engine/evd.ml
index 6dcec2760b..af22de5cd4 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1290,30 +1290,14 @@ module MiniEConstr = struct
   let unsafe_eq = Refl
 
   let to_constr ?(abort_on_undefined_evars=true) sigma c =
-    let rec to_constr c = match Constr.kind c with
-      | Evar ev ->
-        begin match safe_evar_value sigma ev with
-          | Some c -> to_constr c
-          | None ->
-            if abort_on_undefined_evars then
-              anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term")
-            else
-              Constr.map (fun c -> to_constr c) c
-        end
-      | Sort (Sorts.Type u) ->
-        let u' = normalize_universe sigma u in
-        if u' == u then c else mkSort (Sorts.sort_of_univ u')
-      | Const (c', u) when not (Univ.Instance.is_empty u) ->
-        let u' = normalize_universe_instance sigma u in
-        if u' == u then c else mkConstU (c', u')
-      | Ind (i, u) when not (Univ.Instance.is_empty u) ->
-        let u' = normalize_universe_instance sigma u in
-        if u' == u then c else mkIndU (i, u')
-      | Construct (co, u) when not (Univ.Instance.is_empty u) ->
-        let u' = normalize_universe_instance sigma u in
-        if u' == u then c else mkConstructU (co, u')
-      | _ -> Constr.map (fun c -> to_constr c) c
-    in to_constr c
+    let evar_value =
+      if not abort_on_undefined_evars then fun ev -> safe_evar_value sigma ev
+      else fun ev ->
+        match safe_evar_value sigma ev with
+        | Some _ as v -> v
+        | None -> anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term")
+    in
+    Universes.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c
 
   let of_named_decl d = d
   let unsafe_to_named_decl d = d
diff --git a/engine/universes.ml b/engine/universes.ml
index e987087242..0410d1aeaf 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -592,35 +592,6 @@ let subst_univs_constr =
       CProfile.profile2 subst_univs_constr_key subst_univs_constr
   else subst_univs_constr
 
-let subst_univs_fn_puniverses lsubst (c, u as cu) =
-  let u' = Instance.subst_fn lsubst u in
-    if u' == u then cu else (c, u')
-
-let nf_evars_and_universes_opt_subst f subst =
-  let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in
-  let lsubst = level_subst_of subst in
-  let rec aux c =
-    match kind c with
-    | Evar (evk, args) ->
-      let args = Array.map aux args in
-      (match try f (evk, args) with Not_found -> None with
-      | None -> c
-      | Some c -> aux c)
-    | Const pu -> 
-      let pu' = subst_univs_fn_puniverses lsubst pu in
-	if pu' == pu then c else mkConstU pu'
-    | Ind pu ->
-      let pu' = subst_univs_fn_puniverses lsubst pu in
-	if pu' == pu then c else mkIndU pu'
-    | Construct pu ->
-      let pu' = subst_univs_fn_puniverses lsubst pu in
-	if pu' == pu then c else mkConstructU pu'
-    | Sort (Type u) ->
-      let u' = Univ.subst_univs_universe subst u in
-	if u' == u then c else mkSort (sort_of_univ u')
-    | _ -> Constr.map aux c
-  in aux
-
 let fresh_universe_context_set_instance ctx =
   if ContextSet.is_empty ctx then LMap.empty, ctx
   else
@@ -679,6 +650,35 @@ let normalize_opt_subst ctx =
 
 type universe_opt_subst = Universe.t option universe_map
 
+let subst_univs_fn_puniverses f (c, u as cu) =
+  let u' = Instance.subst_fn f u in
+    if u' == u then cu else (c, u')
+
+let nf_evars_and_universes_opt_subst f subst =
+  let subst = normalize_univ_variable_opt_subst (ref subst) in
+  let lsubst = level_subst_of subst in
+  let rec aux c =
+    match kind c with
+    | Evar (evk, args) ->
+      let args = Array.map aux args in
+      (match try f (evk, args) with Not_found -> None with
+      | None -> mkEvar (evk, args)
+      | Some c -> aux c)
+    | Const pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+        if pu' == pu then c else mkConstU pu'
+    | Ind pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+        if pu' == pu then c else mkIndU pu'
+    | Construct pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+        if pu' == pu then c else mkConstructU pu'
+    | Sort (Type u) ->
+      let u' = Univ.subst_univs_universe subst u in
+        if u' == u then c else mkSort (sort_of_univ u')
+    | _ -> Constr.map aux c
+  in aux
+
 let make_opt_subst s = 
   fun x -> 
     (match Univ.LMap.find x s with
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3026be248f..a1c563f536 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -646,7 +646,7 @@ GEXTEND Gram
 
       | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
         pri = OPT [ "|"; i = natural -> i ] ->
-         let info = { hint_priority = pri; hint_pattern = None } in
+         let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in
          let insts = List.map (fun i -> (i, info)) ids in
 	  VernacDeclareInstances insts
 
@@ -771,8 +771,8 @@ GEXTEND Gram
   ;
   hint_info:
     [ [ "|"; i = OPT natural; pat = OPT constr_pattern ->
-         { hint_priority = i; hint_pattern = pat }
-      | -> { hint_priority = None; hint_pattern = None } ] ]
+         { Typeclasses.hint_priority = i; hint_pattern = pat }
+      | -> { Typeclasses.hint_priority = None; hint_pattern = None } ] ]
   ;
   reserv_list:
     [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ]
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 9f186224b9..0fbf2f567f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -260,7 +260,7 @@ module Vernac_ :
     val noedit_mode : vernac_expr Gram.entry
     val command_entry : vernac_expr Gram.entry
     val red_expr : raw_red_expr Gram.entry
-    val hint_info : Vernacexpr.hint_info_expr Gram.entry
+    val hint_info : Typeclasses.hint_info_expr Gram.entry
   end
 
 (** The main entry: reads an optional vernac command *)
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index a5f8060aee..797dfbe23f 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -315,7 +315,7 @@ let project_hint ~poly pri l2r r =
   let ctx = Evd.const_univ_entry ~poly sigma in
   let c = EConstr.to_constr sigma c in
   let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
-  let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
+  let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
     (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
 
 let add_hints_iff ~atts l2r lc n bl =
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 30ddeffa69..e73a78fb84 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -25,6 +25,13 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 (*i*)
 
+(* Core typeclasses hints *)
+type 'a hint_info_gen =
+    { hint_priority : int option;
+      hint_pattern : 'a option }
+
+type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+
 let typeclasses_unique_solutions = ref false
 let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d
 let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions
@@ -73,7 +80,7 @@ type typeclass = {
   cl_props : Context.Rel.t;
 
   (* The method implementaions as projections. *)
-  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option
+  cl_projs : (Name.t * (direction * hint_info_expr) option
 	      * Constant.t option) list;
   
   cl_strict : bool;
@@ -85,7 +92,7 @@ type typeclasses = typeclass Refmap.t
 
 type instance = {
   is_class: global_reference;
-  is_info: Vernacexpr.hint_info_expr;
+  is_info: hint_info_expr;
   (* Sections where the instance should be redeclared,
      None for discard, Some 0 for none. *)
   is_global: int option;
@@ -96,7 +103,7 @@ type instances = (instance Refmap.t) Refmap.t
 
 let instance_impl is = is.is_impl
 
-let hint_priority is = is.is_info.Vernacexpr.hint_priority
+let hint_priority is = is.is_info.hint_priority
 
 let new_instance cl info glob impl =
   let global =
@@ -266,8 +273,6 @@ let check_instance env sigma c =
       not (Evd.has_undefined evd)
   with e when CErrors.noncritical e -> false
 
-open Vernacexpr
-
 let build_subclasses ~check env sigma glob { hint_priority = pri } =
   let _id = Nametab.basename_of_global glob in
   let _next_id = 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index b80c287117..e50d90b156 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -16,6 +16,13 @@ open Environ
 
 type direction = Forward | Backward
 
+(* Core typeclasses hints *)
+type 'a hint_info_gen =
+    { hint_priority : int option;
+      hint_pattern : 'a option }
+
+type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+
 (** This module defines type-classes *)
 type typeclass = {
   (** The toplevel universe quantification in which the typeclass lives. In
@@ -37,7 +44,7 @@ type typeclass = {
       Some may be undefinable due to sorting restrictions or simply undefined if 
       no name is provided. The [int option option] indicates subclasses whose hint has
       the given priority. *)
-  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * Constant.t option) list;
+  cl_projs : (Name.t * (direction * hint_info_expr) option * Constant.t option) list;
 
   (** Whether we use matching or full unification during resolution *)
   cl_strict : bool; 
@@ -55,8 +62,7 @@ val all_instances : unit -> instance list
 
 val add_class : typeclass -> unit
 
-val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool ->
-  global_reference -> instance
+val new_instance : typeclass -> hint_info_expr -> bool -> global_reference -> instance
 val add_instance : instance -> unit
 val remove_instance : instance -> unit
 
@@ -123,16 +129,16 @@ val classes_transparent_state : unit -> transparent_state
 
 val add_instance_hint_hook : 
   (global_reference_or_constr -> global_reference list ->
-   bool (* local? *) -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t
+   bool (* local? *) -> hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t
 val remove_instance_hint_hook : (global_reference -> unit) Hook.t
 val add_instance_hint : global_reference_or_constr -> global_reference list -> 
-  bool -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit
+  bool -> hint_info_expr -> Decl_kinds.polymorphic -> unit
 val remove_instance_hint : global_reference -> unit
 
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
 val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t
 
-val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_reference -> unit
+val declare_instance : hint_info_expr option -> bool -> global_reference -> unit
 
 
 (** Build the subinstances hints for a given typeclass object.
@@ -140,5 +146,5 @@ val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_refere
     subinstances and add only the missing ones. *)
 
 val build_subclasses : check:bool -> env -> evar_map -> global_reference ->
-		       Vernacexpr.hint_info_expr ->
-		       (global_reference list * Vernacexpr.hint_info_expr * constr) list
+                       hint_info_expr ->
+                       (global_reference list * hint_info_expr * constr) list
diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
index 8bf8104983..3a49d6cf83 100644
--- a/pretyping/vernacexpr.ml
+++ b/pretyping/vernacexpr.ml
@@ -112,14 +112,16 @@ type hint_mode =
   | ModeNoHeadEvar (* No evar at the head *)
   | ModeOutput (* Anything *)
 
-type 'a hint_info_gen =
+type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
     { hint_priority : int option;
       hint_pattern : 'a option }
+[@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"]
 
-type hint_info_expr = constr_pattern_expr hint_info_gen
+type hint_info_expr = Typeclasses.hint_info_expr
+[@@ocaml.deprecated "Please use [Typeclasses.hint_info_expr]"]
 
 type hints_expr =
-  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
+  | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
   | HintsImmediate of reference_or_constr list
   | HintsUnfold of reference list
   | HintsTransparency of reference list * bool
@@ -356,12 +358,12 @@ type nonrec vernac_expr =
       local_binder_expr list * (* super *)
 	typeclass_constraint * (* instance name, class name, params *)
 	(bool * constr_expr) option * (* props *)
-	hint_info_expr
+        Typeclasses.hint_info_expr
 
   | VernacContext of local_binder_expr list
 
   | VernacDeclareInstances of
-    (reference * hint_info_expr) list (* instances names, priorities and patterns *)
+    (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *)
 
   | VernacDeclareClass of reference (* inductive or definition name *)
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 89117caf4b..f26ac0bf9a 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -188,7 +188,7 @@ open Pputils
     | ModeNoHeadEvar -> str"!"
     | ModeOutput -> str"-"
 
-  let pr_hint_info pr_pat { hint_priority = pri; hint_pattern = pat } =
+  let pr_hint_info pr_pat { Typeclasses.hint_priority = pri; hint_pattern = pat } =
     pr_opt (fun x -> str"|" ++ int x) pri ++
     pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b11e36bceb..bbcf8def6d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -547,9 +547,9 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
             (List.map_append
              (fun (path,info,c) ->
 	      let info =
-		{ info with Vernacexpr.hint_pattern =
+                { info with hint_pattern =
                             Option.map (Constrintern.intern_constr_pattern env sigma)
-				       info.Vernacexpr.hint_pattern }
+                                       info.hint_pattern }
 	      in
 	      make_resolves env sigma ~name:(PathHints path)
                   (true,false,not !Flags.quiet) info false
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 46d1629119..739f1014a7 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -28,12 +28,13 @@ open Termops
 open Inductiveops
 open Typing
 open Decl_kinds
+open Vernacexpr
+open Typeclasses
 open Pattern
 open Patternops
 open Clenv
 open Tacred
 open Printer
-open Vernacexpr
 
 module NamedDecl = Context.Named.Declaration
 
@@ -94,7 +95,6 @@ let secvars_of_hyps hyps =
   else pred
 
 let empty_hint_info =
-  let open Vernacexpr in
   { hint_priority = None; hint_pattern = None }
 
 (************************************************************************)
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 1811150c2a..b06ede0e16 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -31,7 +31,7 @@ type debug = Debug | Info | Off
 
 val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t
 
-val empty_hint_info : 'a hint_info_gen
+val empty_hint_info : 'a Typeclasses.hint_info_gen
 
 (** Pre-created hint databases *)
 
@@ -144,7 +144,7 @@ type hint_db = Hint_db.t
 
 type hnf = bool
 
-type hint_info = (patvar list * constr_pattern) hint_info_gen
+type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen
 
 type hint_term =
   | IsGlobRef of global_reference
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3a20c3fc46..59c035e83a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -979,6 +979,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
     | LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) ->
         let name = find_name false (LocalDef (name,b,t)) name_flag gl in
 	build_intro_tac name move_flag tac
+    | Evar ev when force_flag ->
+        let sigma, t = Evardefine.define_evar_as_product sigma ev in
+        Tacticals.New.tclTHEN
+          (Proofview.Unsafe.tclEVARS sigma)
+          (intro_then_gen name_flag move_flag force_flag dep_flag tac)
     | _ ->
         begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct))
             (* Note: red_in_concl includes betaiotazeta and this was like *)
diff --git a/test-suite/output/UnclosedBlocks.out b/test-suite/output/UnclosedBlocks.out
index b83e94ad43..31481e84a5 100644
--- a/test-suite/output/UnclosedBlocks.out
+++ b/test-suite/output/UnclosedBlocks.out
@@ -1,3 +1,2 @@
-
 Error: The section Baz, module type Bar and module Foo need to be closed.
 
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index a329894aad..d37ad9f528 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -127,4 +127,28 @@ induction 1 as (n,H,IH).
 exact Logic.I.
 Qed.
 
+(* Make "intro"/"intros" progress on existential variables *)
 
+Module Evar.
+
+Goal exists (A:Prop), A.
+eexists.
+unshelve (intro x).
+- exact nat.
+- exact (x=x).
+- auto.
+Qed.
+
+Goal exists (A:Prop), A.
+eexists.
+unshelve (intros x).
+- exact nat.
+- exact (x=x).
+- auto.
+Qed.
+
+Definition d := ltac:(intro x; exact (x*x)).
+
+Definition d' : nat -> _ := ltac:(intros;exact 0).
+
+End Evar.
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index a1a07fce87..17e848c5af 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -10,8 +10,8 @@
 
 let warning s = Flags.(with_option warn Feedback.msg_warning (Pp.strbrk s))
 
-let fatal_error ?extra exn =
-  Topfmt.print_err_exn ?extra exn;
+let fatal_error exn =
+  Topfmt.print_err_exn Topfmt.ParsingCommandLine exn;
   let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
   exit exit_code
 
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 63b8b538a2..da91695144 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -150,29 +150,28 @@ let print_highlight_location ib loc =
 
 let valid_buffer_loc ib loc =
   let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e
-
 (* Toplevel error explanation. *)
-let error_info_for_buffer ?loc buf =
-  Option.map (fun loc ->
+let error_info_for_buffer ?loc phase buf =
+  match loc with
+  | None -> Topfmt.pr_phase ?loc phase
+  | Some loc ->
       let fname = loc.Loc.fname in
-      let hl, loc =
         (* We are in the toplevel *)
-        match fname with
-        | Loc.ToplevelInput ->
-          let nloc = adjust_loc_buf buf loc in
-          if valid_buffer_loc buf loc then
-            (fnl () ++ print_highlight_location buf nloc, nloc)
-            (* in the toplevel, but not a valid buffer *)
-          else (mt (), nloc)
-          (* we are in batch mode, don't adjust location *)
-        | Loc.InFile _ ->
-           (mt (), loc)
-      in Topfmt.pr_loc loc ++ hl
-    ) loc
+      match fname with
+      | Loc.ToplevelInput ->
+        let nloc = adjust_loc_buf buf loc in
+        if valid_buffer_loc buf loc then
+          match Topfmt.pr_phase ~loc:nloc phase with
+          | None -> None
+          | Some hd -> Some (hd ++ fnl () ++ print_highlight_location buf nloc)
+        (* in the toplevel, but not a valid buffer *)
+        else Topfmt.pr_phase ~loc phase
+      (* we are in batch mode, don't adjust location *)
+      | Loc.InFile _ -> Topfmt.pr_phase ~loc phase
 
 (* Actual printing routine *)
-let print_error_for_buffer ?loc lvl msg buf =
-  let pre_hdr = error_info_for_buffer ?loc buf in
+let print_error_for_buffer ?loc phase lvl msg buf =
+  let pre_hdr = error_info_for_buffer ?loc phase buf in
   if !print_emacs
   then Topfmt.emacs_logger ?pre_hdr lvl msg
   else Topfmt.std_logger   ?pre_hdr lvl msg
@@ -282,7 +281,7 @@ let extract_default_loc loc doc_id sid : Loc.t option =
     with _ -> loc
 
 (** Coqloop Console feedback handler *)
-let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
+let coqloop_feed phase (fb : Feedback.feedback) = let open Feedback in
   match fb.contents with
   | Processed   -> ()
   | Incomplete  -> ()
@@ -301,9 +300,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
   (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *)
   | Message (Warning,loc,msg) ->
     let loc = extract_default_loc loc fb.doc_id fb.span_id in
-    TopErr.print_error_for_buffer ?loc Warning msg top_buffer
+    TopErr.print_error_for_buffer ?loc phase Warning msg top_buffer
   | Message (lvl,loc,msg) ->
-    TopErr.print_error_for_buffer ?loc lvl msg top_buffer
+    TopErr.print_error_for_buffer ?loc phase lvl msg top_buffer
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -353,7 +352,7 @@ let top_goal_print oldp newp =
     let (e, info) = CErrors.push exn in
     let loc = Loc.get_loc info in
     let msg = CErrors.iprint (e, info) in
-    TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer
+    TopErr.print_error_for_buffer ?loc Topfmt.InteractiveLoop Feedback.Error msg top_buffer
 
 (* Careful to keep this loop tail-rec *)
 let rec vernac_loop ~state =
@@ -395,7 +394,7 @@ let rec vernac_loop ~state =
     let (e, info) = CErrors.push any in
     let loc = Loc.get_loc info in
     let msg = CErrors.iprint (e, info) in
-    TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
+    TopErr.print_error_for_buffer ?loc Topfmt.InteractiveLoop Feedback.Error msg top_buffer;
     vernac_loop ~state
 
 let rec loop ~state =
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 39a9de4f83..6d9867fb97 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -30,7 +30,7 @@ val top_buffer : input_buffer
 val set_prompt : (unit -> string) -> unit
 
 (** Toplevel feedback printer. *)
-val coqloop_feed : Feedback.feedback -> unit
+val coqloop_feed : Topfmt.execution_phase -> Feedback.feedback -> unit
 
 (** Main entry point of Coq: read and execute vernac commands. *)
 val loop : state:Vernac.State.t -> Vernac.State.t
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e60382f2ce..38351a377a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -35,12 +35,16 @@ let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s))
 (* Feedback received in the init stage, this is different as the STM
    will not be generally be initialized, thus stateid, etc... may be
    bogus. For now we just print to the console too *)
-let coqtop_init_feed = Coqloop.coqloop_feed
+let coqtop_init_feed = Coqloop.coqloop_feed Topfmt.Initialization
+
+let coqtop_doc_feed = Coqloop.coqloop_feed Topfmt.LoadingPrelude
+
+let coqtop_rcfile_feed = Coqloop.coqloop_feed Topfmt.LoadingRcFile
 
 (* Default toplevel loop *)
 let console_toploop_run opts ~state =
   (* We initialize the console only if we run the toploop_run *)
-  let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in
+  let tl_feed = Feedback.add_feeder (Coqloop.coqloop_feed Topfmt.InteractiveLoop) in
   if Dumpglob.dump () then begin
     Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
     Dumpglob.noglob ()
@@ -101,9 +105,16 @@ let load_vernacular opts ~state =
       else load_vernac s
     ) state (List.rev opts.load_vernacular_list)
 
-let load_init_vernaculars opts ~state =
-  let state = if opts.load_rcfile then
-      Coqinit.load_rcfile ~rcfile:opts.rcfile ~state
+let load_init_vernaculars cur_feeder opts ~state =
+  let state =
+    if opts.load_rcfile then begin
+        Feedback.del_feeder !cur_feeder;
+        let rc_feeder = Feedback.add_feeder coqtop_rcfile_feed in
+        let state  = Coqinit.load_rcfile ~rcfile:opts.rcfile ~state in
+        Feedback.del_feeder rc_feeder;
+        cur_feeder := Feedback.add_feeder coqtop_init_feed;
+        state
+      end
     else begin
       Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
       state
@@ -147,8 +158,8 @@ let fatal_error msg =
   flush_all ();
   exit 1
 
-let fatal_error_exn ?extra exn =
-  Topfmt.print_err_exn ?extra exn;
+let fatal_error_exn exn =
+  Topfmt.print_err_exn Topfmt.Initialization exn;
   flush_all ();
   let exit_code =
     if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1
@@ -194,7 +205,7 @@ let ensure_exists f =
     fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
 (* Compile a vernac file *)
-let compile opts ~echo ~f_in ~f_out =
+let compile cur_feeder opts ~echo ~f_in ~f_out =
   let open Vernac.State in
   let check_pending_proofs () =
     let pfs = Proof_global.get_all_proof_names () in
@@ -218,13 +229,18 @@ let compile opts ~echo ~f_in ~f_out =
         | None -> long_f_dot_v ^ "o"
         | Some f -> ensure_vo long_f_dot_v f in
 
-      let doc, sid = Stm.(new_doc
+      Feedback.del_feeder !cur_feeder;
+      let doc_feeder = Feedback.add_feeder coqtop_doc_feed in
+      let doc, sid =
+        Stm.(new_doc
           { doc_type = VoDoc long_f_dot_vo;
             iload_path; require_libs; stm_options;
           }) in
+      Feedback.del_feeder doc_feeder;
+      cur_feeder := Feedback.add_feeder coqtop_init_feed;
 
       let state = { doc; sid; proof = None; time = opts.time } in
-      let state = load_init_vernaculars opts ~state in
+      let state = load_init_vernaculars cur_feeder opts ~state in
       let ldir = Stm.get_ldir ~doc:state.doc in
       Aux_file.(start_aux_file
         ~aux_file:(aux_file_name_for long_f_dot_vo)
@@ -265,13 +281,18 @@ let compile opts ~echo ~f_in ~f_out =
           async_proofs_tac_error_resilience = `None;
         } in
 
-      let doc, sid = Stm.(new_doc
+      Feedback.del_feeder !cur_feeder;
+      let doc_feeder = Feedback.add_feeder coqtop_doc_feed in
+      let doc, sid =
+        Stm.(new_doc
           { doc_type = VioDoc long_f_dot_vio;
             iload_path; require_libs; stm_options;
           }) in
+      Feedback.del_feeder doc_feeder;
+      cur_feeder := Feedback.add_feeder coqtop_init_feed;
 
       let state = { doc; sid; proof = None; time = opts.time } in
-      let state = load_init_vernaculars opts ~state in
+      let state = load_init_vernaculars cur_feeder opts ~state in
       let ldir = Stm.get_ldir ~doc:state.doc in
       let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in
       let doc = Stm.finish ~doc:state.doc in
@@ -288,21 +309,21 @@ let compile opts ~echo ~f_in ~f_out =
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
       Library.save_library_raw lfdv sum lib univs proofs
 
-let compile opts ~echo ~f_in ~f_out =
+let compile cur_feeder opts ~echo ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
-  compile opts ~echo ~f_in ~f_out;
+  compile cur_feeder opts ~echo ~f_in ~f_out;
   CoqworkmgrApi.giveback 1
 
-let compile_file opts (f_in, echo) =
+let compile_file cur_feeder opts (f_in, echo) =
   if !Flags.beautify then
     Flags.with_option Flags.beautify_file
-      (fun f_in -> compile opts ~echo ~f_in ~f_out:None) f_in
+      (fun f_in -> compile cur_feeder opts ~echo ~f_in ~f_out:None) f_in
   else
-    compile opts ~echo ~f_in ~f_out:None
+    compile cur_feeder opts ~echo ~f_in ~f_out:None
 
-let compile_files opts =
+let compile_files cur_feeder opts =
   let compile_list = List.rev opts.compile_list in
-  List.iter (compile_file opts) compile_list
+  List.iter (compile_file cur_feeder opts) compile_list
 
 (******************************************************************************)
 (* VIO Dispatching                                                            *)
@@ -420,7 +441,7 @@ let init_toplevel arglist =
   CProfile.init_profile ();
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
-  let init_feeder = Feedback.add_feeder coqtop_init_feed in
+  let init_feeder = ref (Feedback.add_feeder coqtop_init_feed) in
   Lib.init();
 
   (* Coq's init process, phase 2:
@@ -489,34 +510,33 @@ let init_toplevel arglist =
         let iload_path = build_load_path opts in
         let require_libs = require_libs opts in
         let stm_options = opts.stm_flags in
-        try
-          let open Vernac.State in
-          let doc, sid =
-            Stm.(new_doc
-                   { doc_type = Interactive opts.toplevel_name;
-                     iload_path; require_libs; stm_options;
-                   }) in
-          let state = { doc; sid; proof = None; time = opts.time } in
-          Some (load_init_vernaculars opts ~state), opts
-        with any -> flush_all(); fatal_error_exn any
+        let open Vernac.State in
+        Feedback.del_feeder !init_feeder;
+        let doc_feeder = Feedback.add_feeder coqtop_doc_feed in
+        let doc, sid =
+          Stm.(new_doc
+                 { doc_type = Interactive opts.toplevel_name;
+                   iload_path; require_libs; stm_options;
+                 }) in
+        Feedback.del_feeder doc_feeder;
+        init_feeder := Feedback.add_feeder coqtop_init_feed;
+        let state = { doc; sid; proof = None; time = opts.time } in
+        Some (load_init_vernaculars init_feeder opts ~state), opts
       (* Non interactive: we perform a sequence of compilation steps *)
       end else begin
-        try
-          compile_files opts;
-          (* Careful this will modify the load-path and state so after
-             this point some stuff may not be safe anymore. *)
-          do_vio opts;
-          (* Allow the user to output an arbitrary state *)
-          outputstate opts;
-          None, opts
-        with any -> flush_all(); fatal_error_exn any
+        compile_files init_feeder opts;
+        (* Careful this will modify the load-path and state so after
+           this point some stuff may not be safe anymore. *)
+        do_vio opts;
+        (* Allow the user to output an arbitrary state *)
+        outputstate opts;
+        None, opts
       end;
     with any ->
       flush_all();
-      let extra = Some (str "Error during initialization: ") in
-      fatal_error_exn ?extra any
+      fatal_error_exn any
   end in
-  Feedback.del_feeder init_feeder;
+  Feedback.del_feeder !init_feeder;
   res
 
 let start () =
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 2e1bd69706..1ac597695f 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -51,7 +51,6 @@ let _ =
        | IsGlobal gr -> Hints.IsGlobRef gr
      in
      let info =
-       let open Vernacexpr in
        { info with hint_pattern =
 		   Option.map
                      (Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env())))
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 0342c840ee..e6134ee5dd 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -22,12 +22,12 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
 
 (** Instance declaration *)
 
-val existing_instance : bool -> reference -> Vernacexpr.hint_info_expr option -> unit
+val existing_instance : bool -> reference -> hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
 val declare_instance_constant :
   typeclass ->
-  Vernacexpr.hint_info_expr -> (** priority *)
+  hint_info_expr -> (** priority *)
   bool -> (** globality *)
   Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(Globnames.global_reference -> unit) ->
@@ -51,7 +51,7 @@ val new_instance :
   ?generalize:bool ->
   ?tac:unit Proofview.tactic  ->
   ?hook:(Globnames.global_reference -> unit) ->
-  Vernacexpr.hint_info_expr ->
+  hint_info_expr ->
   Id.t
 
 (** Setting opacity *)
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 1d720330ac..609dac69aa 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -291,6 +291,14 @@ let init_terminal_output ~color =
 let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning
 
 (* This is specific to the toplevel *)
+
+type execution_phase =
+  | ParsingCommandLine
+  | Initialization
+  | LoadingPrelude
+  | LoadingRcFile
+  | InteractiveLoop
+
 let pr_loc loc =
     let fname = loc.Loc.fname in
     match fname with
@@ -303,13 +311,28 @@ let pr_loc loc =
 	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
 	   str":")
 
-let print_err_exn ?extra any =
+let pr_phase ?loc phase =
+  match phase, loc with
+  | LoadingRcFile, loc ->
+     (* For when all errors go through feedback:
+     str "While loading rcfile:" ++
+     Option.cata (fun loc -> fnl () ++ pr_loc loc) (mt ()) loc *)
+     Option.map pr_loc loc
+  | LoadingPrelude, loc ->
+     Some (str "While loading initial state:" ++ Option.cata (fun loc -> fnl () ++ pr_loc loc) (mt ()) loc)
+  | _, Some loc -> Some (pr_loc loc)
+  | ParsingCommandLine, _
+  | Initialization, _ -> None
+  | InteractiveLoop, _ ->
+     (* Note: interactive messages such as "foo is defined" are not located *)
+     None
+
+let print_err_exn phase any =
   let (e, info) = CErrors.push any in
   let loc = Loc.get_loc info in
-  let msg_loc = Option.cata pr_loc (mt ()) loc in
-  let pre_hdr = pr_opt_no_spc (fun x -> x) extra ++ msg_loc in
+  let pre_hdr = pr_phase ?loc phase in
   let msg = CErrors.iprint (e, info) ++ fnl () in
-  std_logger ~pre_hdr Feedback.Error msg
+  std_logger ?pre_hdr Feedback.Error msg
 
 let with_output_to_file fname func input =
   let channel = open_out (String.concat "." [fname; "out"]) in
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 579b456a28..73dcb0064b 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -53,8 +53,17 @@ val init_terminal_output : color:bool -> unit
 (** Error printing *)
 (* To be deprecated when we can fully move to feedback-based error
    printing. *)
+
+type execution_phase =
+  | ParsingCommandLine
+  | Initialization
+  | LoadingPrelude
+  | LoadingRcFile
+  | InteractiveLoop
+
 val pr_loc : Loc.t -> Pp.t
-val print_err_exn : ?extra:Pp.t -> exn -> unit
+val pr_phase : ?loc:Loc.t -> execution_phase -> Pp.t option
+val print_err_exn : execution_phase -> exn -> unit
 
 (** [with_output_to_file file f x] executes [f x] with logging
     redirected to a file [file] *)