Emilio Jesús Gallego Arias (Oct 25 2021 at 14:35): Emilio Jesús Gallego Arias (Oct 25 2021 at 14:35):Hi folks, do we have a function already that does this?
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
Emilio Jesús Gallego Arias (Oct 25 2021 at 14:35):@Gaëtan Gilbert @Pierre-Marie Pédrot
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)
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]
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?
Emilio Jesús Gallego Arias (Oct 25 2021 at 14:50):TypeOf which is then fed to the printer :)
Enrico Tassi (Oct 25 2021 at 14:59):What is TypeOf ?
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.
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
Gaëtan Gilbert (Oct 25 2021 at 15:12):look at About instead
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.
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: Sep 25 2023 at 11:01 UTC