Stream: Coq devs & plugin devs

Topic: Type of a Global


view this post on Zulip Emilio Jesús Gallego Arias (Oct 25 2021 at 14:35):

Hi folks, do we have a function already that does this?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 25 2021 at 14:35):

val type_of_globref : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> EConstr.t

view this post on Zulip Emilio Jesús Gallego Arias (Oct 25 2021 at 14:35):

@Gaëtan Gilbert @Pierre-Marie Pédrot

view this post on Zulip Gaëtan Gilbert (Oct 25 2021 at 14:42):

no, you can combine Evd.fresh_global and retyping to write it
(although you need to return an evar map for when the ref is univ poly)

view this post on Zulip Enrico Tassi (Oct 25 2021 at 14:48):

The signature is wrong, it should also return an updated evarmap [oops, just saw Gaetan's note]

view this post on Zulip Emilio Jesús Gallego Arias (Oct 25 2021 at 14:49):

Thanks folks, I want it for implementing Typeof , so is discarding the evar_map a safe choice there?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 25 2021 at 14:50):

TypeOf which is then fed to the printer :)

view this post on Zulip Enrico Tassi (Oct 25 2021 at 14:59):

What is TypeOf ?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 25 2021 at 15:02):

A SerAPI query, now that you mention it, I could just look at what Check is doing.

view this post on Zulip Enrico Tassi (Oct 25 2021 at 15:12):

I think the question is: do you want this call to be stateless? If so, protect the vernac state

view this post on Zulip Gaëtan Gilbert (Oct 25 2021 at 15:12):

look at About instead

view this post on Zulip Enrico Tassi (Oct 25 2021 at 15:12):

eg Check ltac:(abstract tt) is pure because the STM says so, not because it actually is.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 25 2021 at 15:39):

I see, thanks for the feedback, the imperative state makes this a bit hard to use indeed.


Last updated: Feb 05 2023 at 20:03 UTC