The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 29/10/2013 17:23, Abhishek Anand wrote:
> I'm writing such a tool for my Coq plugin : https://github.com/aa755/nbcoq
> Given a universe level (e.g. Top.13), is there a way to get the name of
> the definition that contains it?

AFAIK, there is no efficient way to do this. Nonetheless, you can still
search for terms containing it in Coq's current state by using
Declaremods.iter_all_segments, or, in trunk, the higher-level
Search.generic_search.

Then you will need to crawl through the relevant term to find out if it
contains the given universe.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature