[vernac] pass the loc of the whole command to the interp function

5 files changed, 12 insertions, 11 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 481bc3071b..664c6b2f36 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2064,7 +2064,7 @@ let vernac_check_guard ~pstate =
 
 (* We interpret vernacular commands to a DSL that specifies their
    allowed actions on proof states *)
-let translate_vernac ~atts v = let open Vernacextend in match v with
+let translate_vernac ?loc ~atts v = let open Vernacextend in match v with
   | VernacAbortAll
   | VernacRestart
   | VernacUndo _
@@ -2389,4 +2389,4 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
 
   (* Extensions *)
   | VernacExtend (opn,args) ->
-    Vernacextend.type_vernac ~atts opn args
+    Vernacextend.type_vernac ?loc ~atts opn args
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index cf233248d7..4cc58fdd43 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -10,7 +10,8 @@
 
 (** Vernac Translation into the Vernac DSL *)
 val translate_vernac
-  : atts:Attributes.vernac_flags
+  : ?loc:Loc.t
+  -> atts:Attributes.vernac_flags
   -> Vernacexpr.vernac_expr
   -> Vernacextend.typed_vernac
 
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index f320b65954..df82382041 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -64,7 +64,7 @@ type typed_vernac =
   | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t)
   | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t)
 
-type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
+type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> typed_vernac
 
 type plugin_args = Genarg.raw_generic_argument list
 
@@ -94,7 +94,7 @@ let warn_deprecated_command =
 
 (* Interpretation of a vernac command *)
 
-let type_vernac opn converted_args ~atts =
+let type_vernac opn converted_args ?loc ~atts =
   let depr, callback = vinterp_map opn in
   let () = if depr then
       let rules = Egramml.get_extend_vernac_rule opn in
@@ -106,7 +106,7 @@ let type_vernac opn converted_args ~atts =
       warn_deprecated_command pr;
   in
   let hunk = callback converted_args in
-  hunk ~atts
+  hunk ?loc ~atts
 
 (** VERNAC EXTEND registering *)
 
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 070c737882..27f6930dec 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -82,7 +82,7 @@ type typed_vernac =
   | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t)
   | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t)
 
-type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
+type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> typed_vernac
 
 type plugin_args = Genarg.raw_generic_argument list
 
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index e42775b76c..4098401bf0 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -151,7 +151,7 @@ let interp_control_flag ~time_header (f : control_flag) ~st
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
-let rec interp_expr ~atts ~st c =
+let rec interp_expr ?loc ~atts ~st c =
   let stack = st.Vernacstate.lemmas in
   let program = st.Vernacstate.program in
   vernac_pperr_endline Pp.(fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
@@ -174,7 +174,7 @@ let rec interp_expr ~atts ~st c =
     Attributes.unsupported_attributes atts;
     vernac_load ~verbosely fname
   | v ->
-    let fv = Vernacentries.translate_vernac ~atts v in
+    let fv = Vernacentries.translate_vernac ?loc ~atts v in
     interp_typed_vernac ~pm:program ~stack fv
 
 and vernac_load ~verbosely fname =
@@ -206,13 +206,13 @@ and vernac_load ~verbosely fname =
     CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
   stack, pm
 
-and interp_control ~st ({ CAst.v = cmd } as vernac) =
+and interp_control ~st ({ CAst.v = cmd; loc } as vernac) =
   let time_header = mk_time_header vernac in
   List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
     cmd.control
     (fun ~st ->
        let before_univs = Global.universes () in
-       let pstack, pm = interp_expr ~atts:cmd.attrs ~st cmd.expr in
+       let pstack, pm = interp_expr ?loc ~atts:cmd.attrs ~st cmd.expr in
        let after_univs = Global.universes () in
        if before_univs == after_univs then pstack, pm
        else