Merge PR #13844: [vernac] pass the loc of the whole command to the interp function

Reviewed-by: ejgallego

8 files changed, 16 insertions, 14 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 8affe58824..2de103a2ff 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -360,7 +360,7 @@ let print_body_fun state fmt r =
     print_binders r.vernac_toks print_atts_left r.vernac_atts (print_body_state state) r
 
 let print_body state fmt r =
-  fprintf fmt "@[(%afun %a~atts@ -> coqpp_body %a%a)@]"
+  fprintf fmt "@[(%afun %a?loc ~atts@ -> coqpp_body %a%a)@]"
     (print_body_fun state) r print_binders r.vernac_toks
     print_binders r.vernac_toks print_atts_right r.vernac_atts
 
diff --git a/dev/ci/user-overlays/13844-gares-command-loc.sh b/dev/ci/user-overlays/13844-gares-command-loc.sh
new file mode 100644
index 0000000000..d9a1736532
--- /dev/null
+++ b/dev/ci/user-overlays/13844-gares-command-loc.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/LPCIC/coq-elpi command-loc 13844
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f3d6239c6f..f8fd8b3d5b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -576,7 +576,7 @@ let _ =
   let open Vernacextend in
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in
-  let cmd_fn c ~atts = VtDefault (fun () -> in_current_context econstr_display c) in
+  let cmd_fn c ?loc:_ ~atts = VtDefault (fun () -> in_current_context econstr_display c) in
   let cmd_class _ = VtQuery in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   vernac_extend ~command:"PrintConstr" [cmd]
@@ -585,7 +585,7 @@ let _ =
   let open Vernacextend in
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in
-  let cmd_fn c ~atts = VtDefault (fun () -> in_current_context print_pure_econstr c) in
+  let cmd_fn c ?loc:_ ~atts = VtDefault (fun () -> in_current_context print_pure_econstr c) in
   let cmd_class _ = VtQuery in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   vernac_extend ~command:"PrintPureConstr" [cmd]
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 2ac8458ad5..b30bbc3ce7 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