coqc -time prints Derive incorrectly

[JasonGross]

Description of the problem

$ cat foo.v

Require Import Coq.derive.Derive.
Derive foo SuchThat (foo = 1) As foo_eq.
Proof. subst foo; reflexivity. Qed.

$ coqc -q -time foo.v
Chars 0 - 33 [Require~Import~Coq.derive.Derive.] 0. secs (0.u,0.s)
Chars 34 - 74 [Derive~<genarg:identref>~SuchT...] 0. secs (0.u,0.s)
Chars 75 - 81 [Proof.] 0. secs (0.u,0.s)
Chars 82 - 105 [(subst~foo;~reflexivity).] 0. secs (0.u,0.s)
Chars 106 - 110 [Qed.] 0. secs (0.u,0.s)

The <genarg:identref> does not belong.

Coq Version

8.16

[SkySkimmer]

Is that really incorrect?

[JasonGross]

This is not how Definitions print, and it's underinformative. Perhaps "incorrect" was a poor choice of wording, but I do think this is a bug, and wasn't sure how to better describe it

[SkySkimmer]

Derive isn't Obligation
Other commands like Next Obligation of do the same thing.

Anyway it can be changed by adding something like

let register_basic_print0 wit raw glb top =
  register_print0 wit
    (fun x -> PrinterBasic (fun env sigma -> raw x))
    (fun x -> PrinterBasic (fun env sigma -> glb x))
    (fun x -> TopPrinterBasic (fun () -> top x))

let () =
  let open Stdarg in
  let open Names in
  let pr_lident x = Id.print x.CAst.v in
  register_basic_print0 wit_identref pr_lident pr_lident Id.print

at the end of genprint.ml

(and probably similar for the others in

coq/parsing/pcoq.ml

Lines 498 to 508 in 6a8d6f4

	Grammar.register0 wit_nat (Prim.natural);
	Grammar.register0 wit_int (Prim.integer);
	Grammar.register0 wit_string (Prim.string);
	Grammar.register0 wit_pre_ident (Prim.preident);
	Grammar.register0 wit_identref (Prim.identref);
	Grammar.register0 wit_ident (Prim.ident);
	Grammar.register0 wit_hyp (Prim.hyp);
	Grammar.register0 wit_ref (Prim.reference);
	Grammar.register0 wit_smart_global (Prim.smart_global);
	Grammar.register0 wit_sort_family (Constr.sort_family);
	Grammar.register0 wit_constr (Constr.constr);

)

[SkySkimmer]

Make a PR if you want it.