Remove location field from attributes

It was never set, because it makes no sense.

3 files changed, 9 insertions, 12 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 2f1f6e04e3..2bef6ff320 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -14,7 +14,6 @@ let mk_deprecation ?(since=None) ?(note=None) () =
   { since ; note }
 
 type t = {
-  loc : Loc.t option;
   locality : bool option;
   polymorphic : bool;
   template : bool option;
@@ -22,5 +21,5 @@ type t = {
   deprecated : deprecation option;
 }
 
-let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () =
-  { loc ; locality ; polymorphic ; program ; deprecated; template }
+let mk_atts ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () =
+  { locality ; polymorphic ; program ; deprecated; template }
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 571f0ddd7d..b8dcde5655 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -13,7 +13,6 @@ type deprecation = { since : string option ; note : string option }
 val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
 
 type t = {
-  loc : Loc.t option;
   locality : bool option;
   polymorphic : bool;
   template : bool option;
@@ -21,6 +20,6 @@ type t = {
   deprecated : deprecation option;
 }
 
-val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
+val mk_atts : ?locality: bool option ->
   ?polymorphic: bool -> ?template:bool option ->
   ?program: bool -> ?deprecated: deprecation option -> unit -> t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 391e8f7990..57585f11c7 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -740,14 +740,14 @@ let vernac_combined_scheme lid l =
 
 let vernac_universe ~atts l =
   if atts.polymorphic && not (Lib.sections_are_opened ()) then
-    user_err ?loc:atts.loc ~hdr:"vernac_universe"
+    user_err ~hdr:"vernac_universe"
 		 (str"Polymorphic universes can only be declared inside sections, " ++
 		  str "use Monomorphic Universe instead");
   Declare.do_universe atts.polymorphic l
 
 let vernac_constraint ~atts l =
   if atts.polymorphic && not (Lib.sections_are_opened ()) then
-    user_err ?loc:atts.loc ~hdr:"vernac_constraint"
+    user_err ~hdr:"vernac_constraint"
 		 (str"Polymorphic universe constraints can only be declared"
 		  ++ str " inside sections, use Monomorphic Constraint instead");
   Declare.do_constraint atts.polymorphic l
@@ -1721,7 +1721,7 @@ let query_command_selector ?loc = function
       (str "Query commands only support the single numbered goal selector.")
 
 let vernac_check_may_eval ~atts redexp glopt rc =
-  let glopt = query_command_selector ?loc:atts.loc glopt in
+  let glopt = query_command_selector glopt in
   let (sigma, env) = get_current_context_of_args glopt in
   let sigma, c = interp_open_constr env sigma rc in
   let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
@@ -1815,7 +1815,6 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
     print_about env sigma ref_or_by_not udecl
 
 let vernac_print ~atts env sigma =
-  let loc = atts.loc in
   function
   | PrintTables -> print_tables ()
   | PrintFullContext-> print_full_context_typ env sigma
@@ -1863,7 +1862,7 @@ let vernac_print ~atts env sigma =
   | PrintVisibility s ->
     Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s
   | PrintAbout (ref_or_by_not,udecl,glnumopt) ->
-    print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt
+    print_about_hyp_globs ref_or_by_not udecl glnumopt
   | PrintImplicit qid ->
     dump_global qid;
     print_impargs qid
@@ -1929,7 +1928,7 @@ let _ =
       optwrite = (:=) search_output_name_only }
 
 let vernac_search ~atts s gopt r =
-  let gopt = query_command_selector ?loc:atts.loc gopt in
+  let gopt = query_command_selector gopt in
   let r = interp_search_restriction r in
   let env,gopt =
     match gopt with | None ->
@@ -2255,7 +2254,7 @@ let interp ?proof ~atts ~st c =
     let using = Option.append using (Proof_using.get_default_proof_using ()) in
     let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in
     let usings = if Option.is_empty using then "using:no" else "using:yes" in
-    Aux_file.record_in_aux_at ?loc:atts.loc "VernacProof" (tacs^" "^usings);
+    Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
     Option.iter vernac_set_end_tac tac;
     Option.iter vernac_set_used_variables using
   | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]