coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Global reference from string

From: Hans Jacob Fehrmann Rojas <hans.jfehrmann AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Global reference from string
Date: Mon, 2 Jul 2018 05:21:57 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=hans.jfehrmann AT gmail.com; spf=Pass smtp.mailfrom=hans.jfehrmann AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f169.google.com
Ironport-phdr: 9a23:DAHBAB2NpCDMOtyIsmDT+DRfVm0co7zxezQtwd8Zse0TKPad9pjvdHbS+e9qxAeQG9mDtbQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYghEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiCkJOT0k/m/JlsN9l7hUrA67qhFl34LYfIOYOfxjda3dZ9MaQm9BU95TWSNbBIO8dJYEAe4bMulEqInyvEYFoxugCgmsHuPvzyVHhnnw3aYnz+ohFgPG0xY7H9kTt3nUrM/6NKEJUeyvzqnIwyvMb/NM2Tf48ofIdBYhrOqDXbJ1a8XRyE0vGxnZgVWXrIzoJjWY3fkOvWiD9+dsS/6jhmo9pwxyojWj3NkghpTLi44P11zJ9CF0zYAoLtOiUkF7e8SrEJ5IuiGaKYR2RsQiTnltuCkgy70GvYe3fDUQx5g73hLfZeGLfomM7x75W+aRJjB4hH1heL2hnRq97U+gyujkWsm11lZFsDZFn8HSunwR0xHf8MuKR/tn8ku/xDqC1Rrf5vxFLE0wjabbLoQuwr80lpodq0TDGSr2lV32jKCMcEUk4fKk6+bpYrr4pp+cLYp0hRv4MqQogcG/DuE4PRIPX2if4+izyLrj/UjhTLVQkvI2irXZsIzdJckDuqG5BBZV3p8/5Ba7Ejepy88VnWIHLVJAYBKIlZLlO1DIIPDiDPewmU6gkDlxx6OOArq0CZLUa3PHjb3JfLBn6kcaxhBg48pY4sd0A7caaND6UUj7/PLVDgU8Ogqyi9zgCtxmntceUGSURK2XPaPItFaO4MogJuCNYMkevzOreKtt3OLnkXJswQxVRqKux5ZCMCnpTMQjGF2QZD/XuvlEFG4LugQkS+mz0Q+NVDdSYzC5WKduv2hnWrLjNp/KQ8WWuJLExD2yR8QEaWVPC1TKGnDtJd3dBqU8LRmKK8okqQQqELisT4h7i0OrvQ7+jqdudq/ao3NJ853k09dx6qvYkhRgrTE=

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