coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Global reference from string

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Global reference from string
Date: Mon, 2 Jul 2018 11:47:30 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay7-d.mail.gandi.net
Ironport-phdr: 9a23:qhAZYhNfjzIHcHOE0VEl6mtUPXoX/o7sNwtQ0KIMzox0LfT5rarrMEGX3/hxlliBBdydt6oazbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlJiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkaKTA5/mHZhM9+gq1Vrx2upQBwzYHPbYGJN/dzZL/Rcc8USGdDWMtaSixPApm7b4sKF+cPPPxXqJXhp1QUqxuxHQiiBOLryjBTmHD2x7E62PkmHAHJxgMvAc4Ov27SrNnvO6cSUOS1w7LWwjXZc/Nbwiz96IvIcxA6ovGMXLdwcc/Pxkk1DQ/FiEufqZD8Mj6Ty+8DsHCb4vJ+We6yiWMrsQN8riS1yssxiYTEiJgZxk7Y+Sll2Io4JMO0RFRmbdK4DpdcrTyWOoR1T884Xm1luSk3x7sbspChZicK0o4oxxvHZvyHbYeI5hXjWf6LIThmgHJqYrK+ihSr/Ue90OH8U9O70FdOriZfndnDrHYN2AHS6sSdTPty4Fuh1S6O1wDV9O5EPVg5mbTGJ5Mj2LI9lIYfvV7eEiL1lkj6lrGaelk49uSw7uToeLTmppuSN49ujQH+N7wjmsOlDusmLggBRW6b9f6z1L3i+U32W6tFjucqkqTCq5DaJsQaprW6Aw9U14Yj7giwDy283NQeg3YHMEpJeAibgIjxJ1HOPPf4AO+jjFSriTdn3uzJPrn8AprWNXXDi7fgfbNl60FG0gYzzNZf54hVCr4bOv7zVFXx55TkCUoyNBXxyOL6Av180JkfUCSBGPy3KqTX5HCBZf4mJd6jZYsftSzhY6wq7vPyhHl/ll4Zd6SzwbMMa2GjHfVjJkiDJ3zhnoFSQi8xogMiQbmy2xW5WjlJaiPqBvNu1nQAEIujSLz7aMWoib2F0j28G8QINHtFG0uPEHLtep/CXfoQOnvLfp1R1wccXL3kcLcPkAm0vVakmaFkP/HX+ygduIil0tVptbWKyEMCsAdsBsHY6FmjCmF5mmRSGm0s0aR2sBM4xhGG2Kl8xfNRE9BSofVETlViOA==

>How can I get the global one?

Nametab.global or some other Nametab function

> 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

On 02/07/2018 11:21, Hans Jacob Fehrmann Rojas wrote:

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.

[Coq-Club] Global reference from string, Hans Jacob Fehrmann Rojas, 07/02/2018
- Re: [Coq-Club] Global reference from string, Gaëtan Gilbert, 07/02/2018