diff --git a/dev/ci/user-overlays/19584-SkySkimmer-jump-to-def.sh b/dev/ci/user-overlays/19584-SkySkimmer-jump-to-def.sh
new file mode 100644
index 000000000000..0c3f70a5f8de
--- /dev/null
+++ b/dev/ci/user-overlays/19584-SkySkimmer-jump-to-def.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi jump-to-def 19584
diff --git a/interp/abbreviation.ml b/interp/abbreviation.ml
index f3ac0f1def80..c2b03416e72e 100644
--- a/interp/abbreviation.ml
+++ b/interp/abbreviation.ml
@@ -24,6 +24,7 @@ type abbreviation =
     abbrev_onlyparsing : bool;
     abbrev_user_warns : Globnames.extended_global_reference UserWarn.with_qf option;
     abbrev_activated : bool; (* Not really necessary in practice *)
+    abbrev_src : Loc.t option;
   }
 
 let abbrev_table =
@@ -60,7 +61,8 @@ let load_abbreviation i ((sp,kn),(_local,abbrev)) =
     user_err
       (Id.print (basename sp) ++ str " already exists.");
   add_abbreviation kn sp abbrev;
-  Nametab.push_abbreviation ?user_warns:abbrev.abbrev_user_warns (Nametab.Until i) sp kn
+  Nametab.push_abbreviation ?user_warns:abbrev.abbrev_user_warns (Nametab.Until i) sp kn;
+  abbrev.abbrev_src |> Option.iter (fun loc -> Nametab.set_cci_src_loc (Abbrev kn) loc)
 
 let is_alias_of_already_visible_name sp = function
   | _,NRef (ref,None) ->
@@ -108,6 +110,7 @@ let declare_abbreviation ~local user_warns id ~onlyparsing pat =
       abbrev_onlyparsing = onlyparsing;
       abbrev_user_warns = user_warns;
       abbrev_activated = true;
+      abbrev_src = Loc.get_current_command_loc();
     }
   in
   add_leaf (inAbbreviation id (local,abbrev))
diff --git a/lib/loc.ml b/lib/loc.ml
index 2cd61d739160..3c36fc9a9bef 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -114,3 +114,9 @@ let pr loc =
     (str"File " ++ str "\"" ++ str file ++ str "\"" ++
      str", line " ++ int loc.line_nb ++ str", characters " ++
      int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos))
+
+let current_command_loc = ref None
+
+let get_current_command_loc () = !current_command_loc
+
+let set_current_command_loc v = current_command_loc := v
diff --git a/lib/loc.mli b/lib/loc.mli
index f1d948806353..ee108e3c91a5 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -86,3 +86,9 @@ val map : ('a -> 'b) -> 'a located -> 'b located
 
 val pr : t -> Pp.t
 (** Print for user consumption. *)
+
+(** {5 Location of the current command (if any) } *)
+
+val get_current_command_loc : unit -> t option
+
+val set_current_command_loc : t option -> unit
diff --git a/library/nametab.ml b/library/nametab.ml
index fa4061441a36..310a66d7dfe4 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -10,6 +10,7 @@
 
 open Names
 open Libnames
+open Globnames
 
 type object_prefix = {
   obj_dir : DirPath.t;
@@ -400,7 +401,7 @@ struct
       id, (DirPath.repr dir)
 end
 
-module ExtRefEqual = Globnames.ExtRefOrdered
+module ExtRefEqual = ExtRefOrdered
 module MPEqual = Names.ModPath
 
 module ExtRefTab = Make(FullPath)(ExtRefEqual)
@@ -427,11 +428,11 @@ let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab)
 (* Reversed name tables ***************************************************)
 
 (* This table translates extended_global_references back to section paths *)
-type globrevtab = full_path Globnames.ExtRefMap.t
+type globrevtab = full_path ExtRefMap.t
 let the_globrevtab =
-  Summary.ref ~name:"globrevtab" (Globnames.ExtRefMap.empty : globrevtab)
+  Summary.ref ~name:"globrevtab" (ExtRefMap.empty : globrevtab)
 
-let the_globwarntab = Summary.ref ~name:"globwarntag" Globnames.ExtRefMap.empty
+let the_globwarntab = Summary.ref ~name:"globwarntag" ExtRefMap.empty
 
 type mprevtab = DirPath.t MPmap.t
 
@@ -479,9 +480,9 @@ let push_xref ?user_warns visibility sp xref =
   match visibility with
     | Until _ ->
         the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
-        the_globrevtab := Globnames.ExtRefMap.add xref sp !the_globrevtab;
+        the_globrevtab := ExtRefMap.add xref sp !the_globrevtab;
         user_warns |> Option.iter (fun warn ->
-            the_globwarntab := Globnames.ExtRefMap.add xref warn !the_globwarntab)
+            the_globwarntab := ExtRefMap.add xref warn !the_globwarntab)
     | Exactly _ ->
       begin
         assert (Option.is_empty user_warns);
@@ -490,8 +491,8 @@ let push_xref ?user_warns visibility sp xref =
 
 let remove_xref sp xref =
   the_ccitab := ExtRefTab.remove sp !the_ccitab;
-  the_globrevtab := Globnames.ExtRefMap.remove xref !the_globrevtab;
-  the_globwarntab := Globnames.ExtRefMap.remove xref !the_globwarntab
+  the_globrevtab := ExtRefMap.remove xref !the_globrevtab;
+  the_globwarntab := ExtRefMap.remove xref !the_globwarntab
 
 let push_cci ?user_warns visibility sp ref =
   push_xref ?user_warns visibility sp (TrueGlobal ref)
@@ -538,7 +539,7 @@ let path_of_global ref =
   let open GlobRef in
   match ref with
     | VarRef id -> make_path DirPath.empty id
-    | _ -> Globnames.ExtRefMap.find (TrueGlobal ref) !the_globrevtab
+    | _ -> ExtRefMap.find (TrueGlobal ref) !the_globrevtab
 
 let dirpath_of_global ref =
   fst (repr_path (path_of_global ref))
@@ -547,7 +548,7 @@ let basename_of_global ref =
   snd (repr_path (path_of_global ref))
 
 let path_of_abbreviation kn =
-  Globnames.ExtRefMap.find (Abbrev kn) !the_globrevtab
+  ExtRefMap.find (Abbrev kn) !the_globrevtab
 
 let dirpath_of_module mp =
   MPmap.find mp Modules.(!nametab.modrevtab)
@@ -565,7 +566,7 @@ let shortest_qualid_of_global ?loc ctx ref =
   match ref with
     | VarRef id -> make_qualid ?loc DirPath.empty id
     | _ ->
-        let sp =  Globnames.ExtRefMap.find (TrueGlobal ref) !the_globrevtab in
+        let sp =  ExtRefMap.find (TrueGlobal ref) !the_globrevtab in
         ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
 
 let shortest_qualid_of_abbreviation ?loc ctx kn =
@@ -599,7 +600,7 @@ let pr_global_env env ref =
 (* Locate functions *******************************************************)
 
 let pr_depr_xref xref =
-  let sp = Globnames.ExtRefMap.get xref !the_globrevtab in
+  let sp = ExtRefMap.get xref !the_globrevtab in
   pr_qualid (ExtRefTab.shortest_qualid Id.Set.empty sp !the_ccitab)
 
 let pr_depr_ref ref = pr_depr_xref (TrueGlobal ref)
@@ -615,13 +616,13 @@ let warn_deprecated_abbreviation =
   ~pp_qf:pr_depr_xref pr_depr_abbrev
 
 let warn_deprecated_xref ?loc depr = function
-  | Globnames.TrueGlobal ref -> warn_deprecated_ref ?loc (ref, depr)
+  | TrueGlobal ref -> warn_deprecated_ref ?loc (ref, depr)
   | Abbrev a -> warn_deprecated_abbreviation ?loc (a, depr)
 
 let warn_user_warn =
   UserWarn.create_warning ~warning_name_if_no_cats:"warn-reference" ()
 
-let is_warned_xref xref : Globnames.extended_global_reference UserWarn.with_qf option = Globnames.ExtRefMap.find_opt xref !the_globwarntab
+let is_warned_xref xref : extended_global_reference UserWarn.with_qf option = ExtRefMap.find_opt xref !the_globwarntab
 
 let warn_user_warn_xref ?loc user_warns xref =
   user_warns.UserWarn.depr_qf
@@ -669,7 +670,7 @@ let locate_section qid =
 let locate_all qid =
   List.fold_right (fun a l ->
     match a with
-    | Globnames.TrueGlobal a -> a::l
+    | TrueGlobal a -> a::l
     | _ -> l)
     (ExtRefTab.find_prefixes qid !the_ccitab) []
 
@@ -730,3 +731,13 @@ let exists_module dir = MPDTab.exists dir Modules.(!nametab.modtab)
 let exists_modtype sp = MPTab.exists sp Modules.(!nametab.modtypetab)
 
 let exists_universe kn = UnivTab.exists kn !the_univtab
+
+(* Source locations *)
+
+open Globnames
+
+let cci_loc_table : Loc.t ExtRefMap.t ref = Summary.ref ~name:"constant-loc-table" ExtRefMap.empty
+
+let set_cci_src_loc kn loc = cci_loc_table := ExtRefMap.add kn loc !cci_loc_table
+
+let cci_src_loc kn = ExtRefMap.find_opt kn !cci_loc_table
diff --git a/library/nametab.mli b/library/nametab.mli
index 9009838a64bd..a59563f2bfa7 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -174,6 +174,11 @@ val exists_module : DirPath.t -> bool
 val exists_dir : DirPath.t -> bool
 val exists_universe : full_path -> bool
 
+(** {6 These functions declare (resp. return) the source location of the object if known } *)
+
+val set_cci_src_loc : Globnames.extended_global_reference -> Loc.t -> unit
+val cci_src_loc : Globnames.extended_global_reference -> Loc.t option
+
 (** {6 These functions locate qualids into full user names } *)
 
 val full_name_modtype : qualid -> full_path
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 3d8d7eade4c0..f4c2a088451a 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -5,6 +5,7 @@ Arguments Nat.sub (n m)%nat_scope : simpl nomatch
 The reduction tactics unfold Nat.sub but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Stdlib.Init.Nat.sub
+Declared in library Stdlib.Init.Nat, line 71, characters 0-120
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
@@ -13,6 +14,7 @@ The reduction tactics unfold Nat.sub when applied to 1 argument
   but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Stdlib.Init.Nat.sub
+Declared in library Stdlib.Init.Nat, line 71, characters 0-120
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
@@ -22,6 +24,7 @@ The reduction tactics unfold Nat.sub
   when applied to 1 argument but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Stdlib.Init.Nat.sub
+Declared in library Stdlib.Init.Nat, line 71, characters 0-120
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
@@ -30,6 +33,7 @@ The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor and when applied to 2 arguments
 Nat.sub is transparent
 Expands to: Constant Stdlib.Init.Nat.sub
+Declared in library Stdlib.Init.Nat, line 71, characters 0-120
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
@@ -38,6 +42,7 @@ The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor
 Nat.sub is transparent
 Expands to: Constant Stdlib.Init.Nat.sub
+Declared in library Stdlib.Init.Nat, line 71, characters 0-120
 pf :
 forall {D1 C1 : Type},
 (D1 -> C1) -> forall [D2 C2 : Type], (D2 -> C2) -> D1 * D2 -> C1 * C2
@@ -47,6 +52,7 @@ Arguments pf {D1}%foo_scope {C1}%type_scope f [D2 C2] g x : simpl never
 The reduction tactics never unfold pf
 pf is transparent
 Expands to: Constant Arguments.pf
+Declared in library Arguments, line 12, characters 11-13
 fcomp : forall {A B C : Type}, (B -> C) -> (A -> B) -> A -> C
 
 fcomp is not universe polymorphic
@@ -54,6 +60,7 @@ Arguments fcomp {A B C}%type_scope f g x /
 The reduction tactics unfold fcomp when applied to 6 arguments
 fcomp is transparent
 Expands to: Constant Arguments.fcomp
+Declared in library Arguments, line 19, characters 11-16
 volatile : nat -> nat
 
 volatile is not universe polymorphic
@@ -61,6 +68,7 @@ Arguments volatile / x%nat_scope
 The reduction tactics always unfold volatile
 volatile is transparent
 Expands to: Constant Arguments.volatile
+Declared in library Arguments, line 22, characters 11-19
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
@@ -68,6 +76,7 @@ Arguments f x y n%nat_scope v m%nat_scope
 f uses section variables T1 T2.
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
+Declared in library Arguments, line 30, characters 0-147
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
@@ -77,6 +86,7 @@ The reduction tactics unfold f when the 3rd, 4th and
   5th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
+Declared in library Arguments, line 30, characters 0-147
 f : forall [T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
@@ -86,6 +96,7 @@ The reduction tactics unfold f when the 4th, 5th and
   6th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.S1.f
+Declared in library Arguments, line 30, characters 0-147
 f : forall [T1 T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
@@ -94,6 +105,7 @@ The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.f
+Declared in library Arguments, line 30, characters 0-147
      = forall v : unit, f 0 0 5 v 3 = 2
      : Prop
      = 2 = 2
@@ -106,6 +118,7 @@ The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.f
+Declared in library Arguments, line 30, characters 0-147
 forall w : r, w 3 true = tt
      : Prop
 File "./output/Arguments.v", line 52, characters 28-29:
@@ -124,6 +137,7 @@ The reduction tactics always unfold volatilematch
   but avoid exposing match constructs
 volatilematch is transparent
 Expands to: Constant Arguments.volatilematch
+Declared in library Arguments, line 58, characters 11-24
      = fun n : nat => volatilematch n
      : nat -> nat
 *** [ f :
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 001a02f88c82..98b6aafbe27f 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -14,18 +14,21 @@ negb'' is not universe polymorphic
 Arguments negb'' b%bool_scope
 negb'' is transparent
 Expands to: Constant ArgumentsScope.A.B.negb''
+Declared in library ArgumentsScope, line 9, characters 11-17
 negb' : bool -> bool
 
 negb' is not universe polymorphic
 Arguments negb' b%bool_scope
 negb' is transparent
 Expands to: Constant ArgumentsScope.A.negb'
+Declared in library ArgumentsScope, line 6, characters 11-16
 negb : bool -> bool
 
 negb is not universe polymorphic
 Arguments negb b%bool_scope
 negb is transparent
 Expands to: Constant Stdlib.Init.Datatypes.negb
+Declared in library Stdlib.Init.Datatypes, line 66, characters 11-15
 a : bool -> bool
 
 a is not universe polymorphic
@@ -40,18 +43,21 @@ negb is not universe polymorphic
 Arguments negb b
 negb is transparent
 Expands to: Constant Stdlib.Init.Datatypes.negb
+Declared in library Stdlib.Init.Datatypes, line 66, characters 11-15
 negb' : bool -> bool
 
 negb' is not universe polymorphic
 Arguments negb' b
 negb' is transparent
 Expands to: Constant ArgumentsScope.A.negb'
+Declared in library ArgumentsScope, line 6, characters 11-16
 negb'' : bool -> bool
 
 negb'' is not universe polymorphic
 Arguments negb'' b
 negb'' is transparent
 Expands to: Constant ArgumentsScope.A.B.negb''
+Declared in library ArgumentsScope, line 9, characters 11-17
 a : bool -> bool
 
 a is not universe polymorphic
@@ -62,24 +68,28 @@ negb is not universe polymorphic
 Arguments negb b
 negb is transparent
 Expands to: Constant Stdlib.Init.Datatypes.negb
+Declared in library Stdlib.Init.Datatypes, line 66, characters 11-15
 negb' : bool -> bool
 
 negb' is not universe polymorphic
 Arguments negb' b
 negb' is transparent
 Expands to: Constant ArgumentsScope.negb'
+Declared in library ArgumentsScope, line 6, characters 11-16
 negb'' : bool -> bool
 
 negb'' is not universe polymorphic
 Arguments negb'' b
 negb'' is transparent
 Expands to: Constant ArgumentsScope.negb''
+Declared in library ArgumentsScope, line 9, characters 11-17
 f : bool -> bool
 
 f is not universe polymorphic
 Arguments f x%A_scope%B_scope
 f is transparent
 Expands to: Constant ArgumentsScope.f
+Declared in library ArgumentsScope, line 41, characters 11-12
 f tt
      : bool
 f true
@@ -90,6 +100,7 @@ f is not universe polymorphic
 Arguments f x%B_scope%A_scope
 f is transparent
 Expands to: Constant ArgumentsScope.f
+Declared in library ArgumentsScope, line 41, characters 11-12
 f tt
      : bool
 f false
@@ -100,29 +111,34 @@ g is not universe polymorphic
 Arguments g x%A_scope%B_scope
 g is transparent
 Expands to: Constant ArgumentsScope.g
+Declared in library ArgumentsScope, line 64, characters 11-12
 g' : nat -> nat
 
 g' is not universe polymorphic
 Arguments g' x%B_scope%A_scope
 g' is transparent
 Expands to: Constant ArgumentsScope.g'
+Declared in library ArgumentsScope, line 71, characters 11-13
 g'' : unit -> unit
 
 g'' is not universe polymorphic
 Arguments g'' x%B_scope
 g'' is transparent
 Expands to: Constant ArgumentsScope.g''
+Declared in library ArgumentsScope, line 78, characters 11-14
 f : A -> B -> A
 
 f is not universe polymorphic
 Arguments f _%X _%Y
 f is transparent
 Expands to: Constant ArgumentsScope.SectionTest1.S.f
+Declared in library ArgumentsScope, line 91, characters 15-16
 f : A -> B -> A
 
 f is not universe polymorphic
 f is transparent
 Expands to: Constant ArgumentsScope.SectionTest1.f
+Declared in library ArgumentsScope, line 91, characters 15-16
 N.f : A -> A
 
 N.f is not universe polymorphic
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index f44d03dcc2f0..085c39342793 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -23,6 +23,7 @@ eq_refl is template universe polymorphic
 Arguments eq_refl {B}%type_scope {y}, [_] _
   (where some original arguments have been renamed)
 Expands to: Constructor Stdlib.Init.Logic.eq_refl
+Declared in library Stdlib.Init.Logic, line 379, characters 4-11
 Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x.
 
 Arguments myEq B%type_scope x _
@@ -35,6 +36,7 @@ Arguments myrefl {C}%type_scope x _
   (where some original arguments have been renamed)
 myrefl uses section variable A.
 Expands to: Constructor Arguments_renaming.Test1.myrefl
+Declared in library Arguments_renaming, line 25, characters 40-46
 myplus =
 fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   match n with
@@ -54,6 +56,7 @@ The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor
 myplus is transparent
 Expands to: Constant Arguments_renaming.Test1.myplus
+Declared in library Arguments_renaming, line 31, characters 0-108
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 Inductive myEq (A B : Type) (x : A) : A -> Prop :=
@@ -68,6 +71,7 @@ myrefl is template universe polymorphic
 Arguments myrefl A%type_scope {C}%type_scope x _
   (where some original arguments have been renamed)
 Expands to: Constructor Arguments_renaming.myrefl
+Declared in library Arguments_renaming, line 25, characters 40-46
 myrefl
      : forall (A C : Type) (x : A), C -> myEq A C x x
 myplus =
@@ -89,6 +93,7 @@ The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor
 myplus is transparent
 Expands to: Constant Arguments_renaming.myplus
+Declared in library Arguments_renaming, line 31, characters 0-108
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 File "./output/Arguments_renaming.v", line 49, characters 0-36:
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index b76655a39335..defebf2f494c 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -17,11 +17,13 @@ option : Type -> Type
 option is template universe polymorphic
 Arguments option A%type_scope
 Expands to: Inductive Stdlib.Init.Datatypes.option
+Declared in library Stdlib.Init.Datatypes, line 184, characters 10-16
 option : Type@{option.u0} -> Type@{max(Set,option.u0)}
 
 option is template universe polymorphic on option.u0
 Arguments option A%type_scope
 Expands to: Inductive Stdlib.Init.Datatypes.option
+Declared in library Stdlib.Init.Datatypes, line 184, characters 10-16
 File "./output/Inductive.v", line 27, characters 4-13:
 The command has indeed failed with message:
 Parameters should be syntactically the same for each inductive type.
@@ -38,11 +40,13 @@ or is not universe polymorphic
 or may only be eliminated to produce values whose type is SProp or Prop.
 Arguments or (A B)%type_scope
 Expands to: Inductive Stdlib.Init.Logic.or
+Declared in library Stdlib.Init.Logic, line 89, characters 10-12
 sunit : SProp
 
 sunit is not universe polymorphic
 sunit may only be eliminated to produce values whose type is SProp.
 Expands to: Inductive Inductive.sunit
+Declared in library Inductive, line 38, characters 10-15
 sempty@{q | } : Type@{q | Set}
 (* q |  |=  *)
 
@@ -53,6 +57,7 @@ sempty@{q | } may only be eliminated to produce values whose type is in sort qua
   (SProp <= Prop <= Type, and all variables <= Type)
   than the instantiation of q.
 Expands to: Inductive Inductive.sempty
+Declared in library Inductive, line 44, characters 22-28
 ssig@{q1 q2 q3 | a b} :
 forall A : Type@{q1 | a}, (A -> Type@{q2 | b}) -> Type@{q3 | max(a,b)}
 (* q1 q2 q3 | a b |=  *)
@@ -65,6 +70,7 @@ ssig@{q1 q2 q3 | a b} may only be eliminated to produce values whose type is in
   than the instantiation of q3.
 Arguments ssig A%type_scope B%function_scope
 Expands to: Inductive Inductive.ssig
+Declared in library Inductive, line 48, characters 22-26
 BoxP@{q | a} : Type@{q | a} -> Prop
 (* q | a |=  *)
 
@@ -73,3 +79,4 @@ BoxP@{q | a} may only be eliminated to produce values whose type is SProp or Pro
   unless instantiated such that the quality q is SProp or Prop.
 Arguments BoxP A%type_scope
 Expands to: Inductive Inductive.BoxP
+Declared in library Inductive, line 56, characters 22-26
diff --git a/test-suite/output/PrimitiveProjectionsAttribute.out b/test-suite/output/PrimitiveProjectionsAttribute.out
index f6e04f7e1214..47a0f2f4cc72 100644
--- a/test-suite/output/PrimitiveProjectionsAttribute.out
+++ b/test-suite/output/PrimitiveProjectionsAttribute.out
@@ -2,36 +2,44 @@ Foo0 : Type
 
 Foo0 is not universe polymorphic
 Expands to: Inductive PrimitiveProjectionsAttribute.Foo0
+Declared in library PrimitiveProjectionsAttribute, line 3, characters 7-11
 Foo1 : Type
 
 Foo1 is not universe polymorphic
 Foo1 has primitive projections with eta conversion.
 Expands to: Inductive PrimitiveProjectionsAttribute.Foo1
+Declared in library PrimitiveProjectionsAttribute, line 10, characters 7-11
 Foo2 : Type
 
 Foo2 is not universe polymorphic
 Foo2 has primitive projections with eta conversion.
 Expands to: Inductive PrimitiveProjectionsAttribute.Foo2
+Declared in library PrimitiveProjectionsAttribute, line 17, characters 7-11
 Foo3 : Type
 
 Foo3 is not universe polymorphic
 Expands to: Inductive PrimitiveProjectionsAttribute.Foo3
+Declared in library PrimitiveProjectionsAttribute, line 24, characters 7-11
 Foo4 : Type
 
 Foo4 is not universe polymorphic
 Foo4 has primitive projections with eta conversion.
 Expands to: Inductive PrimitiveProjectionsAttribute.Foo4
+Declared in library PrimitiveProjectionsAttribute, line 32, characters 7-11
 Foo5 : Type
 
 Foo5 is not universe polymorphic
 Foo5 has primitive projections with eta conversion.
 Expands to: Inductive PrimitiveProjectionsAttribute.Foo5
+Declared in library PrimitiveProjectionsAttribute, line 39, characters 7-11
 Foo6 : Type
 
 Foo6 is not universe polymorphic
 Foo6 has primitive projections with eta conversion.
 Expands to: Inductive PrimitiveProjectionsAttribute.Foo6
+Declared in library PrimitiveProjectionsAttribute, line 46, characters 7-11
 Foo7 : Type
 
 Foo7 is not universe polymorphic
 Expands to: Inductive PrimitiveProjectionsAttribute.Foo7
+Declared in library PrimitiveProjectionsAttribute, line 53, characters 7-11
diff --git a/test-suite/output/PrimitiveProjectionsAttribute_Records.out b/test-suite/output/PrimitiveProjectionsAttribute_Records.out
index 4f31f18f06eb..b18e69bcc392 100644
--- a/test-suite/output/PrimitiveProjectionsAttribute_Records.out
+++ b/test-suite/output/PrimitiveProjectionsAttribute_Records.out
@@ -3,14 +3,20 @@ B : Set
 B is not universe polymorphic
 B has primitive projections with eta conversion.
 Expands to: Inductive PrimitiveProjectionsAttribute_Records.B
+Declared in
+library PrimitiveProjectionsAttribute_Records, line 5, characters 6-7
 C : Set
 
 C is not universe polymorphic
 C has primitive projections with eta conversion.
 Expands to: Inductive PrimitiveProjectionsAttribute_Records.C
+Declared in
+library PrimitiveProjectionsAttribute_Records, line 10, characters 10-11
 G : Prop
 
 G is not universe polymorphic
 G is in Prop but its eliminators are declared dependent by default
 G has primitive projections without eta conversion.
 Expands to: Inductive PrimitiveProjectionsAttribute_Records.G
+Declared in
+library PrimitiveProjectionsAttribute_Records, line 15, characters 12-13
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index a99f17f8e9e0..8af85e042dbc 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -3,6 +3,7 @@ existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x}
 existT is template universe polymorphic
 Arguments existT [A]%type_scope P%function_scope x _
 Expands to: Constructor Stdlib.Init.Specif.existT
+Declared in library Stdlib.Init.Specif, line 45, characters 4-10
 Inductive sigT (A : Type) (P : A -> Type) : Type :=
     existT : forall x : A, P x -> {x : A & P x}.
 
@@ -20,6 +21,7 @@ eq_refl : forall {A : Type} {x : A}, x = x
 eq_refl is template universe polymorphic
 Arguments eq_refl {A}%type_scope {x}, [_] _
 Expands to: Constructor Stdlib.Init.Logic.eq_refl
+Declared in library Stdlib.Init.Logic, line 379, characters 4-11
 eq_refl : forall {A : Type} {x : A}, x = x
 
 When applied to no arguments:
@@ -41,6 +43,7 @@ Nat.add is not universe polymorphic
 Arguments Nat.add (n m)%nat_scope
 Nat.add is transparent
 Expands to: Constant Stdlib.Init.Nat.add
+Declared in library Stdlib.Init.Nat, line 47, characters 0-113
 Nat.add : nat -> nat -> nat
 
 plus_n_O : forall n : nat, n = n + 0
@@ -49,6 +52,7 @@ plus_n_O is not universe polymorphic
 Arguments plus_n_O n%nat_scope
 plus_n_O is opaque
 Expands to: Constant Stdlib.Init.Peano.plus_n_O
+Declared in library Stdlib.Init.Peano, line 99, characters 6-14
 Inductive le (n : nat) : nat -> Prop :=
     le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m.
 
@@ -59,6 +63,7 @@ comparison : Set
 
 comparison is not universe polymorphic
 Expands to: Inductive Stdlib.Init.Datatypes.comparison
+Declared in library Stdlib.Init.Datatypes, line 333, characters 10-20
 Inductive comparison : Set :=
     Eq : comparison | Lt : comparison | Gt : comparison.
 bar : foo
@@ -78,6 +83,7 @@ Arguments bar {x}
 Module Stdlib.Init.Peano
 Notation sym_eq := eq_sym
 Expands to: Notation Stdlib.Init.Logic.sym_eq
+Declared in library Stdlib.Init.Logic, line 757, characters 0-41
 
 eq_sym : forall [A : Type] [x y : A], x = y -> y = x
 
@@ -85,6 +91,7 @@ eq_sym is not universe polymorphic
 Arguments eq_sym [A]%type_scope [x y] _
 eq_sym is transparent
 Expands to: Constant Stdlib.Init.Logic.eq_sym
+Declared in library Stdlib.Init.Logic, line 419, characters 12-18
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x.
 
 Arguments eq {A}%type_scope x _
@@ -106,13 +113,15 @@ Alias.eq : forall {A : Type}, A -> A -> Prop
 Alias.eq is template universe polymorphic
 Arguments Alias.eq {A}%type_scope x _
 Expands to: Inductive PrintInfos.Alias.eq (syntactically equal to
-Stdlib.Init.Logic.eq)
+            Stdlib.Init.Logic.eq)
+Declared in library Stdlib.Init.Logic, line 378, characters 10-12
 Alias.eq_refl : forall {A : Type} {x : A}, x = x
 
 Alias.eq_refl is template universe polymorphic
 Arguments Alias.eq_refl {A}%type_scope {x}, [_] _
 Expands to: Constructor PrintInfos.Alias.eq_refl (syntactically equal to
-Stdlib.Init.Logic.eq_refl)
+            Stdlib.Init.Logic.eq_refl)
+Declared in library Stdlib.Init.Logic, line 379, characters 4-11
 Alias.eq_ind :
 forall [A : Type] (x : A) (P : A -> Prop), P x -> forall y : A, x = y -> P y
 
@@ -121,7 +130,8 @@ Arguments Alias.eq_ind [A]%type_scope x P%function_scope f y e
   (where some original arguments have been renamed)
 Alias.eq_ind is transparent
 Expands to: Constant PrintInfos.Alias.eq_ind (syntactically equal to
-Stdlib.Init.Logic.eq_ind)
+            Stdlib.Init.Logic.eq_ind)
+Declared in library Stdlib.Init.Logic, line 378, characters 0-115
 fst : forall A B : Type, prod A B -> A
 
 fst is not universe polymorphic
diff --git a/test-suite/output/PrintSecDeps.out b/test-suite/output/PrintSecDeps.out
index 3ef3be36bde3..40bc4d1239a1 100644
--- a/test-suite/output/PrintSecDeps.out
+++ b/test-suite/output/PrintSecDeps.out
@@ -4,19 +4,23 @@ bla is not universe polymorphic
 bla uses section variables A x.
 bla is transparent
 Expands to: Constant PrintSecDeps.S.bla
+Declared in library PrintSecDeps, line 6, characters 13-16
 bli : nat
 
 bli is not universe polymorphic
 bli is transparent
 Expands to: Constant PrintSecDeps.S.bli
+Declared in library PrintSecDeps, line 10, characters 13-16
 bla : forall A : Type, A -> Prop
 
 bla is not universe polymorphic
 Arguments bla A%type_scope x
 bla is transparent
 Expands to: Constant PrintSecDeps.bla
+Declared in library PrintSecDeps, line 6, characters 13-16
 bli : nat
 
 bli is not universe polymorphic
 bli is transparent
 Expands to: Constant PrintSecDeps.bli
+Declared in library PrintSecDeps, line 10, characters 13-16
diff --git a/test-suite/output/Qf_stdlib.out b/test-suite/output/Qf_stdlib.out
index beef0dc2bf53..370407e23b90 100644
--- a/test-suite/output/Qf_stdlib.out
+++ b/test-suite/output/Qf_stdlib.out
@@ -19,6 +19,7 @@ Nat.add is not universe polymorphic
 Arguments Nat.add (n m)%nat_scope
 Nat.add is transparent
 Expands to: Constant Stdlib.Init.Nat.add
+Declared in library Stdlib.Init.Nat, line 47, characters 0-113
 File "./output/Qf_stdlib.v", line 17, characters 6-22:
 Warning: Coq.Init.Nat.add has been replaced by Stdlib.Init.Nat.add.
 [deprecated-dirpath-Coq,deprecated-since-9.0,deprecated,default]
diff --git a/test-suite/output/SchemeNames.out b/test-suite/output/SchemeNames.out
index 953eaaf09b58..702d1960bde7 100644
--- a/test-suite/output/SchemeNames.out
+++ b/test-suite/output/SchemeNames.out
@@ -334,12 +334,14 @@ fooSet_beq is not universe polymorphic
 Arguments fooSet_beq X Y
 fooSet_beq is transparent
 Expands to: Constant SchemeNames.fooSet_beq
+Declared in library SchemeNames, line 160, characters 2-29
 fooSet_eq_dec : forall x y : fooSet, {x = y} + {x <> y}
 
 fooSet_eq_dec is not universe polymorphic
 Arguments fooSet_eq_dec x y
 fooSet_eq_dec is transparent
 Expands to: Constant SchemeNames.fooSet_eq_dec
+Declared in library SchemeNames, line 160, characters 2-29
 internal_fooSet_dec_bl :
 forall x : fooSet,
 (fun x0 : fooSet => forall y : fooSet, fooSet_beq x0 y = true -> x0 = y) x
@@ -348,6 +350,7 @@ internal_fooSet_dec_bl is not universe polymorphic
 Arguments internal_fooSet_dec_bl x y _
 internal_fooSet_dec_bl is transparent
 Expands to: Constant SchemeNames.internal_fooSet_dec_bl
+Declared in library SchemeNames, line 160, characters 2-29
 internal_fooSet_dec_lb :
 forall x : fooSet,
 (fun x0 : fooSet => forall y : fooSet, x0 = y -> fooSet_beq x0 y = true) x
@@ -356,6 +359,7 @@ internal_fooSet_dec_lb is not universe polymorphic
 Arguments internal_fooSet_dec_lb x y _
 internal_fooSet_dec_lb is transparent
 Expands to: Constant SchemeNames.internal_fooSet_dec_lb
+Declared in library SchemeNames, line 160, characters 2-29
 fooType_inds :
 forall P : fooType -> SProp, P aT -> P bT -> forall f1 : fooType, P f1
 
@@ -466,12 +470,14 @@ fooType_beq is not universe polymorphic
 Arguments fooType_beq X Y
 fooType_beq is transparent
 Expands to: Constant SchemeNames.fooType_beq
+Declared in library SchemeNames, line 226, characters 2-30
 fooType_eq_dec : forall x y : fooType, {x = y} + {x <> y}
 
 fooType_eq_dec is not universe polymorphic
 Arguments fooType_eq_dec x y
 fooType_eq_dec is transparent
 Expands to: Constant SchemeNames.fooType_eq_dec
+Declared in library SchemeNames, line 226, characters 2-30
 internal_fooType_dec_bl :
 forall x : fooType,
 (fun x0 : fooType => forall y : fooType, fooType_beq x0 y = true -> x0 = y) x
@@ -480,6 +486,7 @@ internal_fooType_dec_bl is not universe polymorphic
 Arguments internal_fooType_dec_bl x y _
 internal_fooType_dec_bl is transparent
 Expands to: Constant SchemeNames.internal_fooType_dec_bl
+Declared in library SchemeNames, line 226, characters 2-30
 internal_fooType_dec_lb :
 forall x : fooType,
 (fun x0 : fooType => forall y : fooType, x0 = y -> fooType_beq x0 y = true) x
@@ -488,6 +495,7 @@ internal_fooType_dec_lb is not universe polymorphic
 Arguments internal_fooType_dec_lb x y _
 internal_fooType_dec_lb is transparent
 Expands to: Constant SchemeNames.internal_fooType_dec_lb
+Declared in library SchemeNames, line 226, characters 2-30
 F_rect :
 forall (f : Type) (P : F f -> Type),
 (forall f0 : f, P (C f f0)) -> forall f1 : F f, P f1
@@ -496,6 +504,7 @@ F_rect is not universe polymorphic
 Arguments F_rect f%type_scope (P f0)%function_scope f1
 F_rect is transparent
 Expands to: Constant SchemeNames.F_rect
+Declared in library SchemeNames, line 235, characters 0-30
 PP_rect :
 forall (P : Type) (P0 : PP P -> Type),
 (forall p : P, P0 (D P p)) -> forall p : PP P, P0 p
@@ -504,3 +513,4 @@ PP_rect is not universe polymorphic
 Arguments PP_rect P%type_scope (P0 f)%function_scope p
 PP_rect is transparent
 Expands to: Constant SchemeNames.PP_rect
+Declared in library SchemeNames, line 238, characters 0-32
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 30f79650a0b6..a705c9ea04d1 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -259,6 +259,7 @@ forall [A : Type@{JMeq.u0}], A -> forall [B : Type@{JMeq.u1}], B -> Prop
 JMeq is template universe polymorphic on JMeq.u0
 Arguments JMeq [A]%type_scope x [B]%type_scope _
 Expands to: Inductive UnivBinders.PartialTemplate.JMeq
+Declared in library UnivBinders, line 219, characters 10-14
 File "./output/UnivBinders.v", line 234, characters 2-38:
 The command has indeed failed with message:
 Universe u0 already exists.
diff --git a/test-suite/output/Utf8Impargs.out b/test-suite/output/Utf8Impargs.out
index 6c380122b5e1..4672a6fb2272 100644
--- a/test-suite/output/Utf8Impargs.out
+++ b/test-suite/output/Utf8Impargs.out
@@ -4,3 +4,4 @@ id is not universe polymorphic
 Arguments id {A}%type_scope a
 id is transparent
 Expands to: Constant Utf8Impargs.id
+Declared in library Utf8Impargs, line 6, characters 11-13
diff --git a/test-suite/output/bug_15020.out b/test-suite/output/bug_15020.out
index 7957b011c1c9..f12d0f239927 100644
--- a/test-suite/output/bug_15020.out
+++ b/test-suite/output/bug_15020.out
@@ -7,3 +7,4 @@ Arguments eq_rect {A}%type_scope {x} P%function_scope f {y} e
   (where some original arguments have been renamed)
 eq_rect is transparent
 Expands to: Constant Stdlib.Init.Logic.eq_rect
+Declared in library Stdlib.Init.Logic, line 378, characters 0-115
diff --git a/test-suite/output/bug_19702.out b/test-suite/output/bug_19702.out
index d99942318286..f2fc675f8fd8 100644
--- a/test-suite/output/bug_19702.out
+++ b/test-suite/output/bug_19702.out
@@ -4,15 +4,18 @@ f1 is not universe polymorphic
 Arguments f1 {n1}%nat_scope n2%nat_scope w
 f1 is transparent
 Expands to: Constant bug_19702.f1
+Declared in library bug_19702, line 6, characters 11-13
 f1 : ∀ {n1 : nat} [n2 : nat], T n2 → T n1
 
 f1 is not universe polymorphic
 Arguments f1 {n1}%nat_scope [n2]%nat_scope w
 f1 is transparent
 Expands to: Constant bug_19702.f1
+Declared in library bug_19702, line 6, characters 11-13
 f1 : ∀ {n1 n2 : nat}, T n2 → T n1
 
 f1 is not universe polymorphic
 Arguments f1 {n1 n2}%nat_scope w
 f1 is transparent
 Expands to: Constant bug_19702.f1
+Declared in library bug_19702, line 6, characters 11-13
diff --git a/test-suite/output/wish_18097.out b/test-suite/output/wish_18097.out
index 8dfa5abd4d54..d240e862b210 100644
--- a/test-suite/output/wish_18097.out
+++ b/test-suite/output/wish_18097.out
@@ -11,6 +11,7 @@ fix pow (n m : nat) {struct m} : nat :=
 Arguments Nat.pow (n m)%nat_scope
 Notation pow := Nat.pow
 Expands to: Notation wish_18097.pow
+Declared in library wish_18097, line 1, characters 0-24
 
 Nat.pow : nat -> nat -> nat
 
@@ -18,3 +19,4 @@ Nat.pow is not universe polymorphic
 Arguments Nat.pow (n m)%nat_scope
 Nat.pow is transparent
 Expands to: Constant Stdlib.Init.Nat.pow
+Declared in library Stdlib.Init.Nat, line 143, characters 0-117
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 40edf5fee0d2..ef8aadb7f400 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -338,7 +338,7 @@ let declare_instance_program pm env sigma ~locality ~poly name pri impargs udecl
   let uctx = Evd.ustate sigma in
   let kind = Decls.IsDefinition Decls.Instance in
   let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
-  let info = Declare.Info.make  ~udecl ~poly ~kind ~hook () in
+  let info = Declare.Info.make ~udecl ~poly ~kind ~hook () in
   let pm, _ =
     Declare.Obls.add_definition ~pm ~info ~cinfo ~opaque:false ~uctx ~body obls
   in pm
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index dc1b66b53db0..aefa3d7b5010 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -117,7 +117,7 @@ let interp_statement ~program_mode env evd ~flags ~scope name bl typ  =
   let ids = List.map Context.Rel.Declaration.get_name ctx in
   evd, ids, EConstr.it_mkProd_or_LetIn t' ctx, imps @ imps'
 
-let do_definition ?hook ~name ?scope ?clearbody ~poly ?typing_flags ~kind ?using ?user_warns udecl bl red_option c ctypopt =
+let do_definition ?loc ?hook ~name ?scope ?clearbody ~poly ?typing_flags ~kind ?using ?user_warns udecl bl red_option c ctypopt =
   let program_mode = false in
   let env = Global.env() in
   let env = Environ.update_typing_flags ?typing_flags env in
@@ -128,12 +128,12 @@ let do_definition ?hook ~name ?scope ?clearbody ~poly ?typing_flags ~kind ?using
   in
   let kind = Decls.IsDefinition kind in
   let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
-  let info = Declare.Info.make ?scope ?clearbody ~kind ?hook ~udecl ~poly ?typing_flags ?user_warns () in
+  let info = Declare.Info.make ?loc ?scope ?clearbody ~kind ?hook ~udecl ~poly ?typing_flags ?user_warns () in
   let _ : Names.GlobRef.t =
     Declare.declare_definition ~info ~cinfo ~opaque:false ~body ?using evd
   in ()
 
-let do_definition_program ?hook ~pm ~name ~scope ?clearbody ~poly ?typing_flags ~kind ?using ?user_warns udecl bl red_option c ctypopt =
+let do_definition_program ?loc ?hook ~pm ~name ~scope ?clearbody ~poly ?typing_flags ~kind ?using ?user_warns udecl bl red_option c ctypopt =
   let env = Global.env() in
   let env = Environ.update_typing_flags ?typing_flags env in
   (* Explicitly bound universes and constraints *)
@@ -145,11 +145,11 @@ let do_definition_program ?hook ~pm ~name ~scope ?clearbody ~poly ?typing_flags
   Evd.check_univ_decl_early ~poly ~with_obls:true evd udecl [body; typ];
   let pm, _ =
     let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in
-    let info = Declare.Info.make ~udecl ~scope ?clearbody ~poly ~kind ?hook ?typing_flags ?user_warns () in
+    let info = Declare.Info.make ?loc ~udecl ~scope ?clearbody ~poly ~kind ?hook ?typing_flags ?user_warns () in
     Declare.Obls.add_definition ~pm ~info ~cinfo ~opaque:false ~body ~uctx ?using obls
   in pm
 
-let do_definition_interactive ~program_mode ?hook ~name ~scope ?clearbody ~poly ~typing_flags ~kind ?using ?user_warns udecl bl t =
+let do_definition_interactive ?loc ~program_mode ?hook ~name ~scope ?clearbody ~poly ~typing_flags ~kind ?using ?user_warns udecl bl t =
   let env = Global.env () in
   let env = Environ.update_typing_flags ?typing_flags env in
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in
@@ -161,7 +161,7 @@ let do_definition_interactive ~program_mode ?hook ~name ~scope ?clearbody ~poly
   let evd = Evd.minimize_universes evd in
   Pretyping.check_evars_are_solved ~program_mode env evd;
   let typ = EConstr.to_constr evd typ in
-  let info = Declare.Info.make ?hook ~poly ~scope ?clearbody ~kind ~udecl ?typing_flags ?user_warns () in
+  let info = Declare.Info.make ?loc ?hook ~poly ~scope ?clearbody ~kind ~udecl ?typing_flags ?user_warns () in
   let cinfo = Declare.CInfo.make ~name ~typ ~args ~impargs () in
   Evd.check_univ_decl_early ~poly ~with_obls:false evd udecl [typ];
   let evd = if poly then evd else Evd.fix_undefined_variables evd in
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 082073c049b5..7ce8b8b7299e 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -26,7 +26,8 @@ val interp_definition
   -> Evd.evar_map * (EConstr.t * EConstr.t option) * Impargs.manual_implicits
 
 val do_definition
-  :  ?hook:Declare.Hook.t
+  : ?loc:Loc.t
+  -> ?hook:Declare.Hook.t
   -> name:Id.t
   -> ?scope:Locality.definition_scope
   -> ?clearbody:bool
@@ -43,7 +44,8 @@ val do_definition
   -> unit
 
 val do_definition_program
-  :  ?hook:Declare.Hook.t
+  : ?loc:Loc.t
+  -> ?hook:Declare.Hook.t
   -> pm:Declare.OblState.t
   -> name:Id.t
   -> scope:Locality.definition_scope
@@ -61,7 +63,8 @@ val do_definition_program
   -> Declare.OblState.t
 
 val do_definition_interactive
-  :  program_mode:bool
+  : ?loc:Loc.t
+  -> program_mode:bool
   -> ?hook:Declare.Hook.t
   -> name:Id.t
   -> scope:Locality.definition_scope
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 3ee1321d483c..1345e6894af7 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -814,7 +814,7 @@ type t = {
   uctx : Univ.ContextSet.t;
   where_notations : Metasyntax.notation_interpretation_decl list;
   coercions : Libnames.qualid list;
-  indlocs : Loc.t option list;
+  indlocs : DeclareInd.indlocs;
 }
 
 end
@@ -827,7 +827,11 @@ let rec count_binder_expr = function
     Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed here")
 
 let interp_mutual_inductive ~env ~flags ?typing_flags udecl indl ~private_ind ~uniform =
-  let indlocs = List.map (fun ((n,_,_,_),_) -> n.CAst.loc) indl in
+  let indlocs = List.map (fun ((n,_,_,constructors),_) ->
+      let conslocs = List.map (fun (_,(c,_)) -> c.CAst.loc) constructors in
+      n.CAst.loc, conslocs)
+      indl
+  in
   let (params,indl),coercions,ntns = extract_mutual_inductive_declaration_components indl in
   let where_notations = List.map Metasyntax.prepare_where_notation ntns in
   (* Interpret the types *)
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 2a25c25d5746..31ac32281a84 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -59,7 +59,7 @@ type t = {
   uctx : Univ.ContextSet.t;
   where_notations : Metasyntax.notation_interpretation_decl list;
   coercions : Libnames.qualid list;
-  indlocs : Loc.t option list;
+  indlocs : DeclareInd.indlocs;
 }
 
 end
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 412b68e55c9f..a9ebf9fd798b 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -85,15 +85,19 @@ module Info = struct
     ; typing_flags : Declarations.typing_flags option
     ; user_warns : Globnames.extended_global_reference UserWarn.with_qf option
     ; ntns : Metasyntax.notation_interpretation_decl list
+    ; loc : Loc.t option
     }
 
   (** Note that [opaque] doesn't appear here as it is not known at the
      start of the proof in the interactive case. *)
-  let make ?(poly=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition))
+  let make ?loc ?(poly=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition))
       ?(udecl=UState.default_univ_decl) ?(scope=Locality.default_scope)
       ?(clearbody=false) ?hook ?typing_flags ?user_warns ?(ntns=[]) () =
-    { poly; inline; kind; udecl; scope; hook; typing_flags; clearbody; user_warns; ntns }
-
+    let loc = match loc with
+      | None -> Loc.get_current_command_loc()
+      | Some _ -> loc
+    in
+    { poly; inline; kind; udecl; scope; hook; typing_flags; clearbody; user_warns; ntns; loc }
 end
 
 (** Declaration of constants and parameters *)
@@ -384,14 +388,17 @@ type constant_obj = {
   cst_kind : Decls.logical_kind;
   cst_locl : Locality.import_status;
   cst_warn : Globnames.extended_global_reference UserWarn.with_qf option;
+  cst_loc : Loc.t option;
 }
 
 let load_constant i ((sp,kn), obj) =
   if Nametab.exists_cci sp then
     raise (DeclareUniv.AlreadyDeclared (None, Libnames.basename sp));
   let con = Global.constant_of_delta_kn kn in
-  Nametab.push ?user_warns:obj.cst_warn (Nametab.Until i) sp (GlobRef.ConstRef con);
+  let gr = GlobRef.ConstRef con in
+  Nametab.push ?user_warns:obj.cst_warn (Nametab.Until i) sp gr;
   Dumpglob.add_constant_kind con obj.cst_kind;
+  obj.cst_loc |> Option.iter (fun loc -> Nametab.set_cci_src_loc (TrueGlobal gr) loc);
   begin match obj.cst_locl with
     | Locality.ImportNeedQualified -> local_csts := Cset_env.add con !local_csts
     | Locality.ImportDefaultBehavior -> ()
@@ -415,8 +422,10 @@ let check_exists id =
 
 let cache_constant ((sp,kn), obj) =
   let kn = Global.constant_of_delta_kn kn in
-  Nametab.push ?user_warns:obj.cst_warn (Nametab.Until 1) sp (GlobRef.ConstRef kn);
-  Dumpglob.add_constant_kind kn obj.cst_kind
+  let gr = GlobRef.ConstRef kn in
+  Nametab.push ?user_warns:obj.cst_warn (Nametab.Until 1) sp gr;
+  Dumpglob.add_constant_kind kn obj.cst_kind;
+  obj.cst_loc |> Option.iter (fun loc -> Nametab.set_cci_src_loc (TrueGlobal gr) loc)
 
 let discharge_constant obj = Some obj
 
@@ -435,10 +444,10 @@ let (objConstant : (Id.t * constant_obj) Libobject.Dyn.tag) =
 let inConstant v = Libobject.Dyn.Easy.inj v objConstant
 
 (* Register the libobjects attached to the constants *)
-let register_constant cst kind ?user_warns local =
+let register_constant loc cst kind ?user_warns local =
   (* Register the declaration *)
   let id = Label.to_id (Constant.label cst) in
-  let o = inConstant (id, { cst_kind = kind; cst_locl = local; cst_warn = user_warns }) in
+  let o = inConstant (id, { cst_kind = kind; cst_locl = local; cst_warn = user_warns; cst_loc = loc; }) in
   let () = Lib.add_leaf o in
   (* Register associated data *)
   Impargs.declare_constant_implicits cst;
@@ -450,7 +459,7 @@ let register_side_effect (c, body, role) =
   | None -> ()
   | Some opaque -> Opaques.declare_private_opaque opaque
   in
-  let () = register_constant c Decls.(IsProof Theorem) Locality.ImportDefaultBehavior in
+  let () = register_constant (Loc.get_current_command_loc()) c Decls.(IsProof Theorem) Locality.ImportDefaultBehavior in
   match role with
   | None -> ()
   | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme SuperGlobal kind (ind,c)
@@ -548,7 +557,7 @@ let is_unsafe_typing_flags flags =
   let open Declarations in
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
-let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typing_flags ?user_warns cd =
+let declare_constant ~loc ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typing_flags ?user_warns cd =
   let before_univs = Global.universes () in
   let make_constant = function
   (* Logically define the constant and its subproofs, no libobject tampering *)
@@ -642,7 +651,7 @@ let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typi
   in
   let () = DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) ubinders in
   let () = declare_opaque kn delayed in
-  let () = register_constant kn kind local ?user_warns in
+  let () = register_constant loc kn kind local ?user_warns in
   if unsafe || is_unsafe_typing_flags typing_flags then feedback_axiom();
   kn
 
@@ -660,7 +669,7 @@ let declare_private_constant ?role ?(local = Locality.ImportDefaultBehavior) ~na
     else DeclareUniv.declare_univ_binders (ConstRef kn)
         (Monomorphic_entry ctx, UnivNames.empty_binders)
   in
-  let () = register_constant kn kind local in
+  let () = register_constant (Loc.get_current_command_loc()) kn kind local in
   let seff_roles = match role with None -> Cmap.empty | Some r -> Cmap.singleton kn r in
   let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
   kn, eff
@@ -740,7 +749,7 @@ let declare_variable ~name ~kind ~typing_flags d =
             proof_entry_inline_code = de.proof_entry_inline_code;
           }
           in
-          let kn = declare_constant ~name:cname
+          let kn = declare_constant ~name:cname ~loc:None
               ~local:ImportNeedQualified ~kind:(IsProof Lemma) ~typing_flags
               (DefinitionEntry de)
           in
@@ -886,7 +895,7 @@ let declare_definition_scheme ~internal ~univs ~role ~name ?loc c =
   kn, eff
 
 (* Locality stuff *)
-let declare_entry ~name ?(scope=Locality.default_scope) ?(clearbody=false) ~kind ~typing_flags ~user_warns ?hook ?(obls=[]) ~impargs ~uctx entry =
+let declare_entry ~loc ~name ?(scope=Locality.default_scope) ?(clearbody=false) ~kind ~typing_flags ~user_warns ?hook ?(obls=[]) ~impargs ~uctx entry =
   let should_suggest =
     ProofEntry.get_opacity entry
     && not (List.is_empty (Global.named_context()))
@@ -899,7 +908,7 @@ let declare_entry ~name ?(scope=Locality.default_scope) ?(clearbody=false) ~kind
     Names.GlobRef.VarRef name
   | Locality.Global local ->
     assert (not clearbody);
-    let kn = declare_constant ~name ~local ~kind ~typing_flags ?user_warns (DefinitionEntry entry) in
+    let kn = declare_constant ~loc ~name ~local ~kind ~typing_flags ?user_warns (DefinitionEntry entry) in
     let gr = Names.GlobRef.ConstRef kn in
     if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
     gr
@@ -923,7 +932,7 @@ let declare_parameter ~name ~scope ~hook ~impargs ~uctx pe =
   in
   let kind = Decls.(IsAssumption Conjectural) in
   let decl = ParameterEntry pe in
-  let cst = declare_constant ~name ~local ~kind ~typing_flags:None decl in
+  let cst = declare_constant ~loc:None ~name ~local ~kind ~typing_flags:None decl in
   let dref = Names.GlobRef.ConstRef cst in
   let () = Impargs.maybe_declare_manual_implicits false dref impargs in
   let () = assumption_message name in
@@ -962,7 +971,7 @@ let declare_possibly_mutual_definitions ~info ~cinfo ~obls ?(is_telescope=false)
   let _, refs = List.fold_left2_map (fun subst CInfo.{name; impargs} (entry, uctx) ->
       (* replacing matters for Derive-like statement but it does not hurt otherwise *)
       let entry = ProofEntry.map_entry entry ~f:(Vars.replace_vars subst) in
-      let gref = declare_entry ~name ~scope ~clearbody ~kind ?hook ~impargs ~typing_flags ~user_warns ~obls ~uctx entry in
+      let gref = declare_entry ~loc:info.loc ~name ~scope ~clearbody ~kind ?hook ~impargs ~typing_flags ~user_warns ~obls ~uctx entry in
       let inst = instance_of_univs entry.proof_entry_universes in
       let const = Constr.mkRef (gref, inst) in
       ((name, const) :: subst, gref)) [] cinfo entries in
@@ -1314,7 +1323,7 @@ let declare_obligation prg obl ~uctx ~types ~body =
     let ce = definition_entry ?types:ty ~opaque ~univs body in
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
-      declare_constant ~name:obl.obl_name
+      declare_constant ~loc:None ~name:obl.obl_name
         ~typing_flags:prg.prg_info.Info.typing_flags
         ~local:Locality.ImportNeedQualified
         ~kind:Decls.(IsProof Property)
@@ -2270,7 +2279,7 @@ let finish_proved_equations ~pm ~kind ~hook i entries types sigma0 =
         let (body, eff), opaque = match entry.proof_entry_body with Default { body; opaque } -> body, opaque | _ -> assert false in
         let body, typ, args = ProofEntry.shrink_entry local_context body entry.proof_entry_type in
         let entry = { entry with proof_entry_body = Default { body = (body, eff); opaque }; proof_entry_type = typ } in
-        let cst = declare_constant ~name:id ~kind ~typing_flags:None (DefinitionEntry entry) in
+        let cst = declare_constant ~loc:None ~name:id ~kind ~typing_flags:None (DefinitionEntry entry) in
         let sigma, app = Evd.fresh_global (Global.env ()) sigma (GlobRef.ConstRef cst) in
         let sigma = Evd.define ev (EConstr.applist (app, args)) sigma in
         sigma, cst) sigma0
@@ -2793,11 +2802,11 @@ end
 
 module OblState = Obls_.State
 
-let declare_constant ?local ~name ~kind ?typing_flags =
-  declare_constant ?local ~name ~kind ~typing_flags
+let declare_constant ?loc ?local ~name ~kind ?typing_flags =
+  declare_constant ~loc ?local ~name ~kind ~typing_flags
 
-let declare_entry ~name ?scope ~kind ?user_warns ?hook ~impargs ~uctx entry =
-  declare_entry ~name ?scope ~kind ~typing_flags:None ?clearbody:None ~user_warns ?hook ~impargs ~uctx entry
+let declare_entry ?loc ~name ?scope ~kind ?user_warns ?hook ~impargs ~uctx entry =
+  declare_entry ~loc ~name ?scope ~kind ~typing_flags:None ?clearbody:None ~user_warns ?hook ~impargs ~uctx entry
 
 let declare_definition_full ~info ~cinfo ~opaque ~body ?using sigma =
   let c, uctx = declare_definition ~obls:[] ~info ~cinfo ~opaque ~body ?using sigma in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 7be840250ab9..d7dfb58a3da6 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -99,7 +99,8 @@ module Info : sig
   (** Note that [opaque] doesn't appear here as it is not known at the
      start of the proof in the interactive case. *)
   val make
-    : ?poly:bool
+    : ?loc:Loc.t
+    -> ?poly:bool
     -> ?inline : bool
     -> ?kind : Decls.logical_kind
     (** Theorem, etc... *)
@@ -380,7 +381,8 @@ val symbol_entry
     for removal from the public API, use higher-level declare APIs
     instead *)
 val declare_entry
-  :  name:Id.t
+  : ?loc:Loc.t
+  -> name:Id.t
   -> ?scope:Locality.definition_scope
   -> kind:Decls.logical_kind
   -> ?user_warns:Globnames.extended_global_reference UserWarn.with_qf
@@ -437,7 +439,8 @@ val prepare_parameter
   for removal from the public API, use higher-level declare APIs
   instead *)
 val declare_constant
-  :  ?local:Locality.import_status
+  : ?loc:Loc.t
+  -> ?local:Locality.import_status
   -> name:Id.t
   -> kind:Decls.logical_kind
   -> ?typing_flags:Declarations.typing_flags
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index 1e9adfcd575e..fcbecfe136c4 100644
--- a/vernac/declareInd.ml
+++ b/vernac/declareInd.ml
@@ -11,6 +11,8 @@
 open Names
 open Entries
 
+type indlocs = (Loc.t option * Loc.t option list) list
+
 (** Declaration of inductive blocks *)
 let declare_inductive_argument_scopes kn mie =
   List.iteri (fun i {mind_entry_consnames=lc} ->
@@ -20,7 +22,7 @@ let declare_inductive_argument_scopes kn mie =
     done) mie.mind_entry_inds
 
 type inductive_obj = {
-  ind_names : (Id.t * Id.t list) list
+  ind_names : (lident * lident list) list
   (* For each block, name of the type + name of constructors *)
 }
 
@@ -29,30 +31,34 @@ let inductive_names sp kn obj =
   let kn = Global.mind_of_delta_kn kn in
   let names, _ =
     List.fold_left
-      (fun (names, n) (typename, consnames) ->
+      (fun (names, n) ({CAst.v=typename; loc=typeloc}, consnames) ->
          let ind_p = (kn,n) in
          let names, _ =
            List.fold_left
-             (fun (names, p) l ->
+             (fun (names, p) {CAst.v=l; loc} ->
                 let sp = Libnames.make_path dp l in
-                ((sp, GlobRef.ConstructRef (ind_p,p)) :: names, p+1))
-             (names, 1) consnames in
+                ((loc, sp, GlobRef.ConstructRef (ind_p,p)) :: names, p+1))
+             (names, 1) consnames
+         in
          let sp = Libnames.make_path dp typename in
-         ((sp, GlobRef.IndRef ind_p) :: names, n+1))
+         ((typeloc, sp, GlobRef.IndRef ind_p) :: names, n+1))
       ([], 0) obj.ind_names
   in names
 
 let load_inductive i ((sp, kn), names) =
   let names = inductive_names sp kn names in
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
+  List.iter (fun (loc, sp, ref) ->
+      Nametab.push (Nametab.Until i) sp ref;
+      Option.iter (Nametab.set_cci_src_loc (TrueGlobal ref)) loc)
+    names
 
 let open_inductive i ((sp, kn), names) =
   let names = inductive_names sp kn names in
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
+  List.iter (fun (_, sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
 
-let cache_inductive ((sp, kn), names) =
-  let names = inductive_names sp kn names in
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
+let cache_inductive o =
+  (* Until 1 and Exactly 1 are equivalent so no need to open_inductive *)
+  load_inductive 1 o
 
 let discharge_inductive names =
   Some names
@@ -98,15 +104,32 @@ let is_unsafe_typing_flags () =
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
 (* for initial declaration *)
-let declare_mind ?typing_flags mie =
+let declare_mind ?typing_flags ~indlocs mie =
   let id = match mie.mind_entry_inds with
     | ind::_ -> ind.mind_entry_typename
     | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in
-  let map_names mip = (mip.mind_entry_typename, mip.mind_entry_consnames) in
-  let names = List.map map_names mie.mind_entry_inds in
-  List.iter (fun (typ, cons) ->
+  let indlocs = Array.of_list indlocs in
+  let map_names i mip =
+    let typloc, conslocs = if Array.length indlocs <= i then None, []
+      else indlocs.(i)
+    in
+    let typloc = if Option.has_some typloc then typloc else Loc.get_current_command_loc() in
+    let typ = CAst.make ?loc:typloc mip.mind_entry_typename in
+    let conslocs = Array.of_list conslocs in
+    let map_cons j na =
+      let consloc = if Array.length conslocs <= j then None
+        else conslocs.(j)
+      in
+      let consloc = if Option.has_some consloc then consloc else typloc in
+      CAst.make ?loc:consloc na
+    in
+    let consl = List.mapi map_cons mip.mind_entry_consnames in
+    (typ, consl)
+  in
+  let names = List.mapi map_names mie.mind_entry_inds in
+  List.iter (fun ({CAst.v=typ}, cons) ->
       Declare.check_exists typ;
-      List.iter Declare.check_exists cons) names;
+      List.iter (fun {CAst.v} -> Declare.check_exists v) cons) names;
   let mind, why_not_prim_record = Global.add_mind ?typing_flags id mie in
   let () = Lib.add_leaf (inInductive (id, { ind_names = names })) in
   if is_unsafe_typing_flags() then feedback_axiom ();
@@ -178,7 +201,7 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) ?typi
     | _ -> ()
   end;
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
-  let mind, why_not_prim_record = declare_mind ?typing_flags mie in
+  let mind, why_not_prim_record = declare_mind ?typing_flags ~indlocs mie in
   why_not_prim_record |> Option.iter (fun why_not_prim_record ->
       warn_non_primitive_record (mind,why_not_prim_record));
   let () = match fst ubinders with
@@ -216,6 +239,7 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) ?typi
         defaults
   in
   Flags.if_verbose Feedback.msg_info (minductive_message names);
+  let indlocs = List.map fst indlocs in
   let locmap = Ind_tables.Locmap.make mind indlocs in
   if mie.mind_entry_private == None
   then Indschemes.declare_default_schemes mind ~locmap;
diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli
index 108c9e67cdf1..74cf5df2e9de 100644
--- a/vernac/declareInd.mli
+++ b/vernac/declareInd.mli
@@ -17,10 +17,13 @@ type one_inductive_impls =
 
 type default_dep_elim = DefaultElim | PropButDepElim
 
+type indlocs = (Loc.t option * Loc.t option list) list
+(** Inductive type and constructor locs, for .glob and src loc info *)
+
 val declare_mutual_inductive_with_eliminations
   : ?primitive_expected:bool
   -> ?typing_flags:Declarations.typing_flags
-  -> ?indlocs:Loc.t option list (* Inductive type locs, for .glob *)
+  -> ?indlocs:indlocs
   -> ?default_dep_elim:default_dep_elim list
   -> Entries.mutual_inductive_entry (* Inductive types declaration *)
   -> UState.named_universes_entry
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index f1e12bf8f5f3..3f45b0909190 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -904,6 +904,23 @@ let canonical_info env ref =
     | path -> spc() ++ str "(syntactically equal to" ++ spc() ++ pr_path path ++ str ")"
     | exception Not_found -> spc() ++ str "(missing canonical, bug?)"
 
+let pr_loc_use_dp loc = match loc.Loc.fname with
+  | Loc.ToplevelInput ->
+    (* NB emacs mangles the message if it contains the capitalized "Toplevel input" of [Loc.pr] *)
+    str "toplevel input, characters " ++ int loc.bp ++ str "-" ++ int loc.ep
+  | InFile  { dirpath = None } -> Loc.pr loc
+  | InFile { dirpath = Some dp } ->
+    let f = str "library " ++ str dp in
+    (f ++
+     str", line " ++ int loc.line_nb ++ str", characters " ++
+     int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos))
+
+
+let loc_info gr =
+  match Nametab.cci_src_loc gr with
+  | None -> mt()
+  | Some loc -> cut() ++ hov 0 (str "Declared in" ++ spc() ++ pr_loc_use_dp loc)
+
 let pr_located_qualid env = function
   | Term ref ->
       let ref_str = let open GlobRef in match ref with
@@ -913,9 +930,9 @@ let pr_located_qualid env = function
         | VarRef _ -> "Variable"
       in
       let extra = canonical_info env ref in
-      str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref) ++ extra
+      v 0 (hov 0 (str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref) ++ extra))
   | Abbreviation kn ->
-      str "Notation" ++ spc () ++ pr_path (Nametab.path_of_abbreviation kn)
+    str "Notation" ++ spc () ++ pr_path (Nametab.path_of_abbreviation kn)
   | Dir dir ->
       let s,mp =
         let open Nametab in
@@ -1032,7 +1049,8 @@ let print_about_global_reference ?loc env ref udecl =
     print_reduction_behaviour ref @
     print_opacity env ref @
     print_bidi_hints ref @
-    [hov 0 (str "Expands to: " ++ pr_located_qualid env (Term ref))])
+    [hov 0 (str "Expands to: " ++ pr_located_qualid env (Term ref)) ++
+    loc_info (TrueGlobal ref)])
 
 let print_about_abbreviation env sigma kn =
   let (vars,c) = glob_constr_of_abbreviation kn in
@@ -1041,6 +1059,7 @@ let print_about_abbreviation env sigma kn =
   | _ -> [] in
   print_abbreviation_body env kn (vars,c) ++ fnl () ++
   hov 0 (str "Expands to: " ++ pr_located_qualid env (Abbreviation kn)) ++
+  loc_info (Abbrev kn) ++
   with_line_skip pp
 
 let print_about_any ?loc env sigma k udecl =
diff --git a/vernac/record.ml b/vernac/record.ml
index 5a3279a511d5..bce277f82a1e 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -446,6 +446,7 @@ let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramde
   let entry = Declare.definition_entry ~univs ~types:projtyp proj in
   let kind = Decls.IsDefinition kind in
   let kn =
+    (* XXX more precise loc *)
     try Declare.declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry)
     with Type_errors.TypeError (ctx,te) as exn when not primitive ->
       let _, info = Exninfo.capture exn in
@@ -597,7 +598,7 @@ module Record_decl = struct
     ubinders : UnivNames.universe_binders;
     projections_kind : Decls.definition_object_kind;
     poly : bool;
-    indlocs : Loc.t option list;
+    indlocs : DeclareInd.indlocs;
   }
 end
 
@@ -608,7 +609,7 @@ module Ast = struct
     ; is_coercion : coercion_flag
     ; binders: local_binder_expr list
     ; cfs : (local_decl_expr * record_field_attr) list
-    ; idbuild : Id.t
+    ; idbuild : lident
     ; sort : constr_expr option
     ; default_inhabitant_id : Id.t option
     }
@@ -628,14 +629,20 @@ let check_unique_names records =
     | Vernacexpr.DefExpr ({CAst.v=Name id},_,_,_) -> id::acc
     | _ -> acc in
   let indlocs =
-    records |> List.map (fun { Ast.name; _ } -> name ) in
+    records |> List.map (fun { Ast.name; idbuild; _ } -> name, idbuild ) in
   let fields_names =
     records |> List.fold_left (fun acc { Ast.cfs; _ } ->
       List.fold_left extract_name acc cfs) [] in
   let allnames =
-    fields_names @ (indlocs |> List.map (fun x -> x.CAst.v)) in
+    (* XXX we don't check the name of the constructor ([idbuild])
+       because definitional classes ignore it so it being a duplicate must be allowed.
+
+       Maybe we will refactor this someday, or maybe we will remove
+       the early check and let declaration fail when there are duplicates. *)
+    fields_names @ (indlocs |> List.map (fun (x,_) -> x.CAst.v))
+  in
   match List.duplicates Id.equal allnames with
-  | [] -> List.map (fun x -> x.CAst.loc) indlocs
+  | [] -> List.map (fun (x,y) -> x.CAst.loc, [y.CAst.loc]) indlocs
   | id :: _ -> user_err (str "Two objects have the same name" ++ spc () ++ quote (Id.print id) ++ str ".")
 
 type kind_class = NotClass | RecordClass | DefClass
@@ -736,7 +743,7 @@ let pre_process_structure ~auto_prop_lowering udecl kind ~poly (records : Ast.t
         Namegen.next_ident_away canonical_inhabitant_id (bound_names_rdata rdata)
     in
     let is_coercion = match is_coercion with AddCoercion -> true | NoCoercion -> false in
-    { Data.id = name.CAst.v; idbuild; rdata; is_coercion; proj_flags; inhabitant_id }
+    { Data.id = name.CAst.v; idbuild = idbuild.v; rdata; is_coercion; proj_flags; inhabitant_id }
   in
   let data = List.map2 map data records in
   let projections_kind =
diff --git a/vernac/record.mli b/vernac/record.mli
index 4ca94fdb3062..6012881fb583 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -19,7 +19,7 @@ module Ast : sig
     ; is_coercion : coercion_flag
     ; binders: local_binder_expr list
     ; cfs : (local_decl_expr * record_field_attr) list
-    ; idbuild : Id.t
+    ; idbuild : lident
     ; sort : constr_expr option
     ; default_inhabitant_id : Id.t option
     }
@@ -68,7 +68,7 @@ val definition_structure
       ubinders : UnivNames.universe_binders;
       projections_kind : Decls.definition_object_kind;
       poly : bool;
-      indlocs : Loc.t option list;
+      indlocs : DeclareInd.indlocs;
     }
 end
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7cd25a4dc633..6267bda276d0 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -840,7 +840,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, udecl) bl t =
   let canonical_instance, reversible = atts.canonical_instance, atts.reversible in
   let hook = vernac_definition_hook ~canonical_instance ~local ~poly ~reversible kind in
   let name = vernac_definition_name lid scope in
-  ComDefinition.do_definition_interactive ~typing_flags ~program_mode ~name ~poly ~scope ?clearbody:atts.clearbody
+  ComDefinition.do_definition_interactive ?loc:lid.loc ~typing_flags ~program_mode ~name ~poly ~scope ?clearbody:atts.clearbody
     ~kind:(Decls.IsDefinition kind) ?user_warns ?using:atts.using ?hook udecl bl t
 
 let vernac_definition ~atts ~pm (discharge, kind) (lid, udecl) bl red_option c typ_opt =
@@ -858,12 +858,12 @@ let vernac_definition ~atts ~pm (discharge, kind) (lid, udecl) bl red_option c t
       Some (snd (Redexpr.interp_redexp_no_ltac env sigma r)) in
   if program_mode then
     let kind = Decls.IsDefinition kind in
-    ComDefinition.do_definition_program ~pm ~name
+    ComDefinition.do_definition_program ?loc:lid.loc ~pm ~name
       ?clearbody ~poly ?typing_flags ~scope ~kind
       ?user_warns ?using udecl bl red_option c typ_opt ?hook
   else
     let () =
-      ComDefinition.do_definition ~name
+      ComDefinition.do_definition ~name ?loc:lid.loc
         ?clearbody ~poly ?typing_flags ~scope ~kind
         ?user_warns ?using udecl bl red_option c typ_opt ?hook in
     pm
@@ -878,11 +878,11 @@ let vernac_start_proof ~atts kind l =
   List.iter (fun ((id, _), _) -> check_name_freshness scope id) l;
   match l with
   | [] -> assert false
-  | [({v=name},udecl),(bl,typ)] ->
-    ComDefinition.do_definition_interactive
+  | [({v=name; loc},udecl),(bl,typ)] ->
+    ComDefinition.do_definition_interactive ?loc
       ~typing_flags ~program_mode ~name ~poly ?clearbody ~scope
       ~kind:(Decls.IsProof kind) ?user_warns ?using udecl bl typ
-  | _ ->
+  | ((lid,_),_) :: _ ->
     let fix = List.map (fun ((fname, univs), (binders, rtype)) ->
         { fname; binders; rtype; body_def = None; univs; notations = []}) l in
     let pm, proof =
@@ -974,8 +974,8 @@ let should_treat_as_uniform () =
 let vernac_record ~template udecl ~cumulative k ~poly ?typing_flags ~primitive_proj finite ?mode records =
   let map ((is_coercion, name), binders, sort, nameopt, cfs, ido) =
     let idbuild = match nameopt with
-    | None -> Nameops.add_prefix "Build_" name.v
-    | Some lid -> lid.v
+    | None -> CAst.map (Nameops.add_prefix "Build_") name
+    | Some lid -> lid
     in
     let default_inhabitant_id = Option.map (fun CAst.{v=id} -> id) ido in
     Record.Ast.{ name; is_coercion; binders; cfs; idbuild; sort; default_inhabitant_id }
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 0eab3f97aa93..b7b79bc2e3a3 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -106,9 +106,14 @@ and vernac_load ~verbosely entries =
   stack, pm
 
 and interp_control ~st ({ CAst.v = cmd; loc }) =
-  interp_control_gen ~loc ~st cmd.control
-    ~unfreeze_transient:Vernacstate.Synterp.unfreeze
-    (fun () -> interp_expr ?loc ~st cmd)
+  Util.try_finally (fun () ->
+      Loc.set_current_command_loc loc;
+      interp_control_gen ~loc ~st cmd.control
+        ~unfreeze_transient:Vernacstate.Synterp.unfreeze
+        (fun () -> interp_expr ?loc ~st cmd))
+    ()
+    (fun () -> Loc.set_current_command_loc None)
+    ()
 
 (* XXX: This won't properly set the proof mode, as of today, it is
    controlled by the STM. Thus, we would need access information from