diff --git a/CHANGES.md b/CHANGES.md
index 783f6da8e..65fa9f8a8 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -49,6 +49,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
   duplicated directory component.
 - LSP server: go-to-definition and hover on qualified identifiers, and session
   state leaking between open documents.
+- LSP server: the success ("OK") diagnostic of a command or tactic is now
+  shown on its introducing keyword ("symbol", "rule", "assume", …), instead
+  of underlining the whole command or tactic (symbol body, rule right-hand
+  side, proof, etc.).
 
 ## 3.0.0 (2025-07-16)
 
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index fac04645c..0ed9822ea 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -28,7 +28,8 @@ let sig_state_of_require l : Sig_state.sig_state =
     Handle.Command.handle Compile.compile ss
      (Pos.none
       (Parsing.Syntax.P_require
-        (Some false, [Pos.none (Parsing.Parser.path_of_string req)]))))
+        (Some false,
+         [Pos.none (Parsing.Parser.path_of_string req)]))))
   Core.Sig_state.dummy l
 
 let search_cmd cfg rules require s dbpath_opt =
diff --git a/src/common/pos.ml b/src/common/pos.ml
index aa251026e..75dd7b852 100644
--- a/src/common/pos.ml
+++ b/src/common/pos.ml
@@ -112,6 +112,16 @@ let cat : popt -> popt -> popt = fun p1 p2 ->
   | None, Some p -> Some p
   | None, None -> None
 
+(** [prefix n p] is the sub-position of [p] covering only its first [n]
+    characters, which are assumed to lie on the first line of [p] and to be
+    ASCII (so that [n] is both a column count and a character count). *)
+let prefix : int -> popt -> popt = fun n p ->
+  match p with
+  | None -> None
+  | Some p -> Some { p with end_line = p.start_line
+                          ; end_col = p.start_col + n
+                          ; end_offset = p.start_offset + n }
+
 (** [shift k p] returns a position that is [k] characters after [p].
     /!\ The generated position may not actually exist in the user input.
     The fields start_offset, end_offset and end_col are inconsistent. *)
diff --git a/src/export/coq.ml b/src/export/coq.ml
index 6defb5ba5..c9d438918 100644
--- a/src/export/coq.ml
+++ b/src/export/coq.ml
@@ -114,9 +114,9 @@ and typopt oc t = Option.iter (prefix " : " term oc) t
 
 let command oc {elt; pos} =
   begin match elt with
-  | P_open(true,ps) ->
+  | P_open(_,true,ps) ->
       string oc "Import "; list path " " oc ps; string oc ".\n"
-  | P_open(false,ps) ->
+  | P_open(_,false,ps) ->
       string oc "Export "; list path " " oc ps; string oc ".\n"
   | P_require (None, ps) ->
       string oc "Require "; list path " " oc ps; string oc ".\n"
@@ -129,7 +129,7 @@ let command oc {elt; pos} =
     string oc "Module "; ident oc i; string oc " := "; path oc p;
     string oc ".\n"
   | P_symbol
-    { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ;
+    { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ;
       p_sym_trm; p_sym_prf=_; p_sym_def } ->
       if not (is_mapped p_sym_nam.elt) then
         begin match p_sym_def, p_sym_trm, p_sym_arg, p_sym_typ with
diff --git a/src/export/lean.ml b/src/export/lean.ml
index 6aebe4d46..cb00be6ca 100644
--- a/src/export/lean.ml
+++ b/src/export/lean.ml
@@ -140,7 +140,7 @@ let openings = ref []
 
 let command oc {elt; pos} =
   begin match elt with
-  | P_open(_,ps) -> List.iter (open_mod oc) ps
+  | P_open(_,_,ps) -> List.iter (open_mod oc) ps
   | P_require(b,ps) ->
       List.iter (req_mod oc) ps;
       begin
@@ -149,8 +149,8 @@ let command oc {elt; pos} =
         | _ -> () (*FIXME?*)
       end
   | P_require_as(p,i) -> Stt.alias := StrMap.add i.elt p.elt !Stt.alias
-  | P_symbol { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm;
-               p_sym_prf=_; p_sym_def } ->
+  | P_symbol { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ;
+               p_sym_trm; p_sym_prf=_; p_sym_def } ->
     if not (is_mapped p_sym_nam.elt) then
         begin match p_sym_def, p_sym_trm, p_sym_arg, p_sym_typ with
           | true, Some t, _, Some a when List.exists is_lem p_sym_mod ->
diff --git a/src/export/rawdk.ml b/src/export/rawdk.ml
index b9b917e67..174d7f04e 100644
--- a/src/export/rawdk.ml
+++ b/src/export/rawdk.ml
@@ -198,7 +198,7 @@ let command : p_command pp = fun ppf ({elt; pos} as c) ->
   | P_query q -> query ppf q
   | P_require(None,ps) ->
       List.iter (fun {elt;_} -> out ppf "#REQUIRE %a@." Dk.mident elt) ps
-  | P_symbol{p_sym_mod; p_sym_nam=n; p_sym_arg; p_sym_typ;
+  | P_symbol{p_sym_mod; p_sym_kw=_; p_sym_nam=n; p_sym_arg; p_sym_typ;
              p_sym_trm; p_sym_prf=None; p_sym_def=_;} ->
       let ms = partition_modifiers p_sym_mod in
       begin match get_ac_typ pos ms p_sym_arg p_sym_typ with
diff --git a/src/handle/command.ml b/src/handle/command.ml
index de0938aa0..f76edfdfa 100644
--- a/src/handle/command.ml
+++ b/src/handle/command.ml
@@ -250,7 +250,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
   | P_require(bo,ps) ->
       (List.fold_left (handle_require compile bo) ss ps, None, None)
   | P_require_as(p,id) -> (handle_require_as compile ss p id, None, None)
-  | P_open(b,ps) -> (List.fold_left (handle_open b) ss ps, None, None)
+  | P_open(_,b,ps) -> (List.fold_left (handle_open b) ss ps, None, None)
   | P_rules(rs) ->
     (* Scope rules, and check that they preserve typing. Return the list of
        rules [srs] and also a [map] mapping every symbol defined by a rule
@@ -345,7 +345,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
       Console.out 2 (Color.gre "coercion %a") sym_rule r;
       (ss, None, None)
 
-  | P_inductive(ms, params, p_ind_list) ->
+  | P_inductive(_, ms, params, p_ind_list) ->
       (* Check modifiers. *)
       let (prop, expo, mstrat, opaq) = handle_modifiers ms in
       if prop <> Defin then
@@ -444,8 +444,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
         rec_sym_list;
       (ss, None, None)
 
-  | P_symbol {p_sym_mod;p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm;p_sym_prf;
-              p_sym_def} ->
+  | P_symbol {p_sym_mod;p_sym_kw=_;p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm;
+              p_sym_prf;p_sym_def} ->
     (* We check that the identifier is not already used. *)
     let {elt=id; _} = p_sym_nam in
     if Sign.mem ss.signature id then
diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml
index d7f0f87c4..11449acaa 100644
--- a/src/lsp/lp_doc.ml
+++ b/src/lsp/lp_doc.ml
@@ -22,7 +22,7 @@ module LSP = Lsp_base
 let lp_logger = Buffer.create 100
 
 type doc_node =
-  { ast   : Pure.Command.t
+  { cmd   : Pure.Command.t
   ; exec  : bool
   (*; tactics : Proof.Tactic.t list*)
   ; goals : (Goal.info list * Pos.popt) list
@@ -63,7 +63,10 @@ let process_pstep (pstate,diags,logs) tac nb_subproofs =
   | Tac_OK (pstate, qres) ->
     let goals = Some (current_goals pstate) in
     let qres = match qres with None -> "OK" | Some x -> x in
-    pstate, (tac_loc, 4, qres, goals) :: diags, logs
+    (* Show the success hint on the tactic's leading keyword only. This
+       tuple also anchors the goals panel (see [get_goals]), whose lookup
+       reads the start of the position: the start must not move. *)
+    pstate, (Tactic.keyword_pos tac, 4, qres, goals) :: diags, logs
   | Tac_Error(loc,msg) ->
     let loc = option_default loc tac_loc in
     let goals = Some (current_goals pstate) in
@@ -83,27 +86,32 @@ let get_goals dg_proof =
   in get_goals_aux [] dg_proof
 (* XXX: Imperative problem *)
 
-let process_cmd _file (nodes,st,dg,logs) ast =
+let process_cmd _file (nodes,st,dg,logs) cmd =
   let open Pure in
   (* let open Timed in *)
   (* XXX: Capture output *)
   (* Console.out_fmt := lp_fmt;
    * Console.err_fmt := lp_fmt; *)
-  let cmd_loc = Command.get_pos ast in
-  let hndl_cmd_res = handle_command st ast in
+  let cmd_loc = Command.get_pos cmd in
+  let hndl_cmd_res = handle_command st cmd in
   let logs = ((3, buf_get_and_clear lp_logger), cmd_loc) :: logs in
   match hndl_cmd_res with
   | Cmd_OK (st, qres) ->
     let qres = match qres with None -> "OK" | Some x -> x in
-    let nodes = { ast; exec = true; goals = [] } :: nodes in
-    let ok_diag = cmd_loc, 4, qres, None in
+    let nodes = { cmd; exec = true; goals = [] } :: nodes in
+    (* Show the success hint on the command's introducing keyword only. *)
+    let ok_diag = Command.keyword_pos cmd, 4, qres, None in
     nodes, st, ok_diag :: dg, logs
   | Cmd_Proof (pst, tlist, thm_loc, qed_loc) ->
     let start_goals = current_goals pst in
     let pst, dg_proof, logs = process_proof pst tlist logs in
-    let dg_proof = (thm_loc, 4, "OK", Some start_goals) :: dg_proof in
-    let goals = get_goals dg_proof in
-    let nodes = { ast; exec = true; goals } :: nodes in
+    (* Initial goals stay anchored at the symbol, for the goals panel. *)
+    let goals =
+      get_goals ((thm_loc, 4, "OK", Some start_goals) :: dg_proof) in
+    let nodes = { cmd; exec = true; goals } :: nodes in
+    (* Visible success hint on the "symbol" keyword, not on the symbol
+       name. *)
+    let dg_proof = (Command.keyword_pos cmd, 4, "OK", None) :: dg_proof in
     let st, dg_proof, logs =
       match end_proof pst with
       | Cmd_OK (st, qres)   ->
@@ -123,7 +131,7 @@ let process_cmd _file (nodes,st,dg,logs) ast =
     nodes, st, dg_proof @ dg, logs
 
   | Cmd_Error(loc, msg) ->
-    let nodes = { ast; exec = false; goals = [] } :: nodes in
+    let nodes = { cmd; exec = false; goals = [] } :: nodes in
     let cmd_loc, loc, diag, log = match cmd_loc, loc with
     | Some l, Some Some l' ->
         if l.fname = l'.fname then
diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml
index 22d76b2f6..a9b0847bc 100644
--- a/src/lsp/lp_lsp.ml
+++ b/src/lsp/lp_lsp.ml
@@ -222,8 +222,8 @@ let in_range ?loc (line, pos) =
 
 let get_node_at_pos doc line pos =
   let open Lp_doc in
-  List.find_opt (fun { ast; _ } ->
-      let loc = Pure.Command.get_pos ast in
+  List.find_opt (fun { cmd; _ } ->
+      let loc = Pure.Command.get_pos cmd in
       in_range ?loc (line,pos)
     ) doc.Lp_doc.nodes
 
diff --git a/src/parsing/dkParser.mly b/src/parsing/dkParser.mly
index 8e5e867b6..3196e9c4d 100644
--- a/src/parsing/dkParser.mly
+++ b/src/parsing/dkParser.mly
@@ -49,6 +49,7 @@
     let symbol lps p_sym_mod i ps p_sym_typ p_sym_trm =
       make_pos lps (P_symbol
         { p_sym_mod
+        ; p_sym_kw = None (* Dedukti has no "symbol" keyword. *)
         ; p_sym_nam = p_ident i
         ; p_sym_arg = List.map (fun (i,t) -> params i (Some t)) ps
         ; p_sym_typ
diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml
index 9f953b0ed..65fdc1d0a 100644
--- a/src/parsing/lpParser.ml
+++ b/src/parsing/lpParser.ml
@@ -436,15 +436,20 @@ let term_id (lb:'token lexbuf): p_term =
 (* [req] tells whether the command starts with the [require] keyword:
    [require [private] open] loads the modules and opens them
    ([P_require]), while a bare [[private] open] only opens modules
-   that are already loaded ([P_open]). *)
+   that are already loaded ([P_open]). For a bare open, the position
+   of the "open" keyword is recorded in the AST (a "private" modifier,
+   like modifiers of symbol declarations, is not part of the
+   keyword). *)
 let open_ (req:bool) (priv:bool) (lb:'token lexbuf) : p_command_aux =
  if log_enabled() then log "%s" __FUNCTION__;
+ let kw_pos = Some(locate (current_pos lb)) in
  consume OPEN lb;
  let ps = nelist path_tks path lb in
- if req then P_require(Some priv,ps) else P_open(priv,ps)
+ if req then P_require(Some priv,ps) else P_open(kw_pos,priv,ps)
 
 let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux =
  if log_enabled() then log "%s" __FUNCTION__;
+ let p_sym_kw = Some(locate (current_pos lb)) in
  consume SYMBOL lb;
  let p_sym_nam = uid lb in
  let p_sym_arg = list params_tks params lb in
@@ -460,7 +465,7 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux =
              let p_sym_prf = Some (proof lb) in
              let p_sym_def = false in
              let sym =
-               {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ;
+               {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ;
                 p_sym_trm=None; p_sym_def; p_sym_prf}
              in P_symbol(sym)
          | ASSIGN ->
@@ -468,7 +473,7 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux =
              let p_sym_trm, p_sym_prf = term_proof lb in
              let p_sym_def = true in
              let sym =
-               {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ;
+               {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ;
                 p_sym_trm; p_sym_def; p_sym_prf}
              in P_symbol(sym)
          | SEMICOLON ->
@@ -476,7 +481,7 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux =
              let p_sym_def = false in
              let p_sym_prf = None in
              let sym =
-               {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ;
+               {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ;
                 p_sym_trm; p_sym_def; p_sym_prf}
              in P_symbol(sym)
          | _ ->
@@ -488,7 +493,7 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux =
        let p_sym_def = true in
        let p_sym_typ = None in
        let sym =
-         {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ;
+         {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ;
           p_sym_trm; p_sym_def; p_sym_prf}
        in P_symbol(sym)
    | _ ->
@@ -501,10 +506,11 @@ and inductive_cmd (p_sym_mod:p_modifier list) (lb:'token lexbuf)
  let xs = list params_tks params lb in
  match current_token lb with
  | INDUCTIVE ->
+     let kw_pos = Some(locate (current_pos lb)) in
      consume INDUCTIVE lb;
      let i = inductive lb in
      let is = list [WITH] (prefix WITH inductive) lb in
-     P_inductive(p_sym_mod,xs,i::is)
+     P_inductive(kw_pos,p_sym_mod,xs,i::is)
  | _ -> expected lb "" [L_PAREN;L_SQ_BRACKET;INDUCTIVE]
 
 and command (lb:'token lexbuf) : p_command =
diff --git a/src/parsing/parser.ml b/src/parsing/parser.ml
index df74b37c3..547c2cf57 100644
--- a/src/parsing/parser.ml
+++ b/src/parsing/parser.ml
@@ -75,7 +75,7 @@ module Dk : PARSER with type lexbuf := Lexing.lexbuf = struct
     parse_lexbuf None entry lb
 
   let command =
-    let r = ref (Pos.none (P_open(false,[]))) in
+    let r = ref (Pos.none (P_open(None,false,[]))) in
     fun (lb:lexbuf): p_command ->
     Debug.(record_time Parsing
              (fun () -> r := DkParser.line DkLexer.token lb)); !r
diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml
index 6a1b790f0..f120de2f5 100644
--- a/src/parsing/pretty.ml
+++ b/src/parsing/pretty.ml
@@ -367,16 +367,16 @@ let proof : (p_proof * p_proof_end) pp = fun ppf (p, pe) ->
 let command : p_command pp = fun ppf { elt; _ } ->
   begin match elt with
   | P_builtin (s, qid) -> out ppf "@[builtin \"%s\"@ ≔ %a@]" s qident qid
-  | P_inductive (_, _, []) -> assert false (* not possible *)
-  | P_inductive (ms, xs, i :: il) ->
+  | P_inductive (_, _, _, []) -> assert false (* not possible *)
+  | P_inductive (_, ms, xs, i :: il) ->
     let with_ind ppf i = out ppf "@,%a" (inductive "with") i in
     out ppf "@[<v>@[%a%a@]%a%a@]"
       modifiers ms (List.pp params " ") xs
       (inductive "inductive") i (List.pp with_ind "") il
   | P_notation (qid, n) ->
     out ppf "notation %a %a" qident qid (Print.notation string) n
-  | P_open(false,ps) -> out ppf "open %a" (List.pp path " ") ps
-  | P_open(true,ps) -> out ppf "private open %a" (List.pp path " ") ps
+  | P_open(_,false,ps) -> out ppf "open %a" (List.pp path " ") ps
+  | P_open(_,true,ps) -> out ppf "private open %a" (List.pp path " ") ps
   | P_query q -> query ppf q
   | P_require (None, ps) -> out ppf "require %a" (List.pp path " ") ps
   | P_require (Some false, ps) ->
@@ -389,7 +389,7 @@ let command : p_command pp = fun ppf { elt; _ } ->
     let with_rule ppf r = out ppf "@.%a" (rule "with") r in
     rule "rule" ppf r; List.iter (with_rule ppf) rs
   | P_symbol
-    { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ;
+    { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ;
       p_sym_trm; p_sym_prf; p_sym_def } ->
     begin
       out ppf "@[<v>@[<2>%asymbol %a%a%a%a%a@]%a@]"
diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml
index be3357f14..91fa648e9 100644
--- a/src/parsing/syntax.ml
+++ b/src/parsing/syntax.ml
@@ -298,6 +298,63 @@ and p_tactic = p_tactic_aux loc
 (** [is_destructive t] says whether tactic [t] changes the current goal. *)
 let is_destructive {elt;_} = match elt with P_tac_have _ -> false | _ -> true
 
+(** [query_keyword q] returns the keyword introducing query [q]. *)
+let query_keyword : p_query -> string = fun {elt;_} ->
+  match elt with
+  | P_query_verbose _ -> "verbose"
+  | P_query_debug _ -> "debug"
+  | P_query_flag _ -> "flag"
+  | P_query_assert(true,_) -> "assertnot"
+  | P_query_assert(false,_) -> "assert"
+  | P_query_infer _ -> "type"
+  | P_query_normalize _ -> "compute"
+  | P_query_prover _ -> "prover"
+  | P_query_prover_timeout _ -> "prover_timeout"
+  | P_query_print _ -> "print"
+  | P_query_proofterm -> "proofterm"
+  | P_query_search _ -> "search"
+
+(** [tactic_keyword t] returns the keyword introducing tactic [t], or
+    [None] for tactics that no single keyword introduces (not produced by
+    the LP parser). *)
+let tactic_keyword : p_tactic -> string option = fun {elt;_} ->
+  match elt with
+  | P_tac_admit -> Some "admit"
+  | P_tac_and _ -> None
+  | P_tac_all_hyps _ -> Some "all_hyps"
+  | P_tac_apply _ -> Some "apply"
+  | P_tac_assume _ -> Some "assume"
+  | P_tac_assumption -> Some "assumption"
+  | P_tac_change _ -> Some "change"
+  | P_tac_eval _ -> Some "eval"
+  | P_tac_fail -> Some "fail"
+  | P_tac_first_hyp _ -> Some "first_hyp"
+  | P_tac_focus _ -> Some "focus"
+  | P_tac_generalize _ -> Some "generalize"
+  | P_tac_have _ -> Some "have"
+  | P_tac_induction -> Some "induction"
+  | P_tac_orelse _ -> Some "orelse"
+  | P_tac_query q -> Some (query_keyword q)
+  | P_tac_refine _ -> Some "refine"
+  | P_tac_refl -> Some "reflexivity"
+  | P_tac_remove _ -> Some "remove"
+  | P_tac_repeat _ -> Some "repeat"
+  | P_tac_rewrite _ -> Some "rewrite"
+  | P_tac_set _ -> Some "set"
+  | P_tac_simpl _ -> Some "simplify"
+  | P_tac_solve -> Some "solve"
+  | P_tac_sym -> Some "symmetry"
+  | P_tac_try _ -> Some "try"
+  | P_tac_why3 _ -> Some "why3"
+
+(** [tactic_keyword_pos t] returns the position of the keyword introducing
+    tactic [t], or the position of the whole of [t] when no single keyword
+    does. *)
+let tactic_keyword_pos : p_tactic -> Pos.popt = fun ({pos;_} as t) ->
+  match tactic_keyword t with
+  | Some kw -> Pos.prefix (String.length kw) pos
+  | None -> pos
+
 (** Parser-level representation of a proof. *)
 type p_subproof = p_proofstep list
 
@@ -337,6 +394,7 @@ let is_priv {elt; _} = match elt with P_expo Privat -> true | _ -> false
 (** Parser-level representation of symbol declarations. *)
 type p_symbol =
   { p_sym_mod : p_modifier list (** modifiers *)
+  ; p_sym_kw : Pos.popt (** position of the "symbol" keyword *)
   ; p_sym_nam : p_ident (** symbol name *)
   ; p_sym_arg : p_params list (** arguments before ":" *)
   ; p_sym_typ : p_term option (** symbol type *)
@@ -348,10 +406,12 @@ type p_symbol =
 type p_command_aux =
   | P_require  of (*private?*)bool (*open?*)option * p_path list
   | P_require_as of p_path * p_ident
-  | P_open of (*private?*)bool * p_path list
+  | P_open of (*"open" keyword position*)Pos.popt
+              * (*private?*)bool * p_path list
   | P_symbol of p_symbol
   | P_rules of p_rule list
-  | P_inductive of p_modifier list * p_params list * p_inductive list
+  | P_inductive of (*"inductive" keyword position*)Pos.popt
+                   * p_modifier list * p_params list * p_inductive list
   | P_builtin of string * p_qident
   | P_notation of p_qident * string Term.notation
   | P_unif_rule of p_rule
@@ -362,6 +422,29 @@ type p_command_aux =
 (** Parser-level representation of a single (located) command. *)
 type p_command = p_command_aux loc
 
+(** [command_keyword_pos c] returns the position of the keyword introducing
+    command [c] ("symbol", "rule", "require", …). Symbol, inductive and
+    open commands record it in the AST, as modifiers or parameters may
+    precede their keyword; for the other commands it is a prefix of the
+    position of [c]. When no position was recorded (e.g. on Dedukti input),
+    the position of the whole of [c] is returned instead. *)
+let command_keyword_pos : p_command -> Pos.popt = fun {elt; pos} ->
+  let prefix kw = Pos.prefix (String.length kw) pos in
+  match elt with
+  | P_open(kw,_,_)
+  | P_inductive(kw,_,_,_)
+  | P_symbol{p_sym_kw=kw;_} ->
+      (match kw with Some _ -> kw | None -> pos)
+  | P_require _
+  | P_require_as _ -> prefix "require"
+  | P_rules _ -> prefix "rule"
+  | P_builtin _ -> prefix "builtin"
+  | P_notation _ -> prefix "notation"
+  | P_unif_rule _ -> prefix "unif_rule"
+  | P_coercion _ -> prefix "coerce_rule"
+  | P_query q -> prefix (query_keyword q)
+  | P_opaque _ -> prefix "opaque"
+
 (** Top level AST returned by the parser. *)
 type ast = p_command Stream.t
 
@@ -493,12 +576,12 @@ let eq_p_sym_prf : (p_proof * p_proof_end) eq = fun (p1, pe1) (p2, pe2) ->
   pe1.elt = pe2.elt && eq_p_proof p1 p2
 
 let eq_p_symbol : p_symbol eq = fun
-  { p_sym_mod=p_sym_mod1; p_sym_nam=p_sym_nam1; p_sym_arg=p_sym_arg1;
-    p_sym_typ=p_sym_typ1; p_sym_trm=p_sym_trm1; p_sym_prf=p_sym_prf1;
-    p_sym_def=p_sym_def1}
-  { p_sym_mod=p_sym_mod2; p_sym_nam=p_sym_nam2; p_sym_arg=p_sym_arg2;
-    p_sym_typ=p_sym_typ2; p_sym_trm=p_sym_trm2; p_sym_prf=p_sym_prf2;
-    p_sym_def=p_sym_def2} ->
+  { p_sym_mod=p_sym_mod1; p_sym_kw=_; p_sym_nam=p_sym_nam1;
+    p_sym_arg=p_sym_arg1; p_sym_typ=p_sym_typ1; p_sym_trm=p_sym_trm1;
+    p_sym_prf=p_sym_prf1; p_sym_def=p_sym_def1}
+  { p_sym_mod=p_sym_mod2; p_sym_kw=_; p_sym_nam=p_sym_nam2;
+    p_sym_arg=p_sym_arg2; p_sym_typ=p_sym_typ2; p_sym_trm=p_sym_trm2;
+    p_sym_prf=p_sym_prf2; p_sym_def=p_sym_def2} ->
   List.eq eq_p_modifier p_sym_mod1 p_sym_mod2
   && eq_p_ident p_sym_nam1 p_sym_nam2
   && List.eq eq_p_params p_sym_arg1 p_sym_arg2
@@ -511,13 +594,14 @@ let eq_p_symbol : p_symbol eq = fun
     are compared up to source code positions. *)
 let eq_p_command : p_command eq = fun {elt=c1;_} {elt=c2;_} ->
   match c1, c2 with
-  | P_require(b1,l1), P_require(b2,l2) -> b1 = b2 && List.eq eq_p_path l1 l2
-  | P_open(b1,l1), P_open(b2,l2) -> b1 = b2 && List.eq eq_p_path l1 l2
+  | P_require(b1,l1), P_require(b2,l2) ->
+      b1 = b2 && List.eq eq_p_path l1 l2
+  | P_open(_,b1,l1), P_open(_,b2,l2) -> b1 = b2 && List.eq eq_p_path l1 l2
   | P_require_as(m1,i1), P_require_as(m2,i2) ->
       eq_p_path m1 m2 && eq_p_ident i1 i2
   | P_symbol s1, P_symbol s2 -> eq_p_symbol s1 s2
   | P_rules(r1), P_rules(r2) ->  List.eq eq_p_rule r1 r2
-  | P_inductive(m1,xs1,l1), P_inductive(m2,xs2,l2) ->
+  | P_inductive(_,m1,xs1,l1), P_inductive(_,m2,xs2,l2) ->
       m1 = m2 && List.eq eq_p_params xs1 xs2
       && List.eq eq_p_inductive l1 l2
   | P_builtin(s1,q1), P_builtin(s2,q2) -> s1 = s2 && eq_p_qident q1 q2
@@ -717,7 +801,7 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a =
     | P_coercion r
     | P_unif_rule r -> fold_rule a r
     | P_rules rs -> List.fold_left fold_rule a rs
-    | P_inductive (_, xs, ind_list) ->
+    | P_inductive (_, _, xs, ind_list) ->
         let vs, a = List.fold_left fold_args (StrSet.empty, a) xs in
         List.fold_left (fold_inductive_vars vs) a ind_list
     | P_symbol {p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm;p_sym_prf;_} ->
diff --git a/src/pure/pure.ml b/src/pure/pure.ml
index 2efd2f992..422cd26e3 100644
--- a/src/pure/pure.ml
+++ b/src/pure/pure.ml
@@ -22,6 +22,7 @@ module Command = struct
   (* TODO: Fixme not to use generic equality *)
   let equal_with_pos = (=)
   let get_pos c = Pos.(c.pos)
+  let keyword_pos = Syntax.command_keyword_pos
   let print = Util.located Pretty.command
 end
 
@@ -47,6 +48,7 @@ module Tactic = struct
   type t = Syntax.p_tactic
   let equal = Syntax.eq_p_tactic
   let get_pos t = Pos.(t.pos)
+  let keyword_pos = Syntax.tactic_keyword_pos
   let print = Util.located Pretty.tactic
 end
 
diff --git a/src/pure/pure.mli b/src/pure/pure.mli
index b865e9f71..0634f3c7f 100644
--- a/src/pure/pure.mli
+++ b/src/pure/pure.mli
@@ -10,6 +10,10 @@ module Command : sig
   type t
   val equal : t -> t -> bool
   val get_pos : t -> Pos.popt
+  val keyword_pos : t -> Pos.popt
+  (** Position of the keyword introducing the command ("symbol", "rule",
+      "require", …), which is not always at its start: modifiers or
+      parameters may precede it. *)
   val print : t Base.pp [@@ocaml.toplevel_printer]
 end
 
@@ -20,6 +24,9 @@ module Tactic : sig
   type t
   val equal : t -> t -> bool
   val get_pos : t -> Pos.popt
+  val keyword_pos : t -> Pos.popt
+  (** Position of the keyword introducing the tactic, or of the whole
+      tactic when no single keyword does. *)
   val print : t Base.pp [@@ocaml.toplevel_printer]
 end