[Coq-Club] Global reference from string

[Hans Jacob Fehrmann Rojas]

Hi everyone,

Currently I'm developing a plugin. At some point, I need to get the global
reference of some definition but I only have the string used to define it
(actually is an id). How can I get the global one?

Also, in the same spirit, eventually I will need to add a term with a name
but will only have string.

Thanks,
Hans.

[Gaëtan Gilbert]

Post by Hans Jacob Fehrmann Rojas
How can I get the global one?

Nametab.global or some other Nametab function

Post by Hans Jacob Fehrmann Rojas
Also, in the same spirit, eventually I will need to add a term with a
name but will only have string.

If you mean add a definition look at the Declare API (eg
Declare.declare_constant) and DeclareDef (higher level API than Declare)
If that's not what you mean then please explain more.

Gaëtan Gilbert

Post by Hans Jacob Fehrmann Rojas
Hi everyone,
Currently I'm developing a plugin. At some point, I need to get the
global reference of some definition but I only have the string used to
define it (actually is an id). How can I get the global one?
Also, in the same spirit, eventually I will need to add a term with a
name but will only have string.
Thanks,
Hans.