Stream: Elpi users & devs

Topic: Local version of coq.locate


view this post on Zulip Enzo Crance (Nov 19 2022 at 16:39):

Hello.
Is there a local version of coq.locate? The documentation states that it looks for a global reference.
I would like to open a module, declare a record, and access its fields in subsequent declarations. When running coq.locate on the name of the field (which is supposed to be a function declared right after the inductive that stands for the record), I get nothing, as if the field projector did not exist.

view this post on Zulip Enrico Tassi (Nov 19 2022 at 20:23):

that is weird, it should work. open an issue please


Last updated: Mar 28 2024 at 15:01 UTC