`coq.gr->string` duplicates the identifier about coq-elpi HOT 2 CLOSED

I was expecting coq.gr->string GR KIdent to give a kernel name KIdent such that coq.locate KIdent GR, which is how I understand the doc:

Elpi Command debug.
Elpi Query debug lp:{{
  coq.locate "bool" GR,                     % ok
  coq.locate "Coq.Init.Datatypes.bool" GR', % ok
  coq.gr->string GR ID,                     % ID = Coq.Init.Datatypes.bool.bool
  coq.locate ID GR''                        % fails
}}.

Also coq.gr->path seems to suffer the same problem, except there is no such thing as acoq.path->gr to test that one cancels the other...

from coq-elpi.

Not 100% sure of recalling why I did it like that, but the code does it on purpose :-)
Unfortunately I did not bind mutual inductives yet, so I can't test this easily, but my guess is that
it would print ...even.even and ...even.odd for example, since the first part comes from the block of mutual inductives while the second from the name of the single inductive (in the inductive block).
It prints ....bool.bool.true for constructors as well...

coq.gr->id probably does what you want.

I leave this open since I don't know what to do. If I remove the duplication I'm afraid that it would print the same for both even and odd, that is not something you want.

from coq-elpi.