Hi folks, do we have a function already that does this?
val type_of_globref : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> EConstr.t
@Gaëtan Gilbert @Pierre-Marie Pédrot
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)
The signature is wrong, it should also return an updated evarmap [oops, just saw Gaetan's note]
Thanks folks, I want it for implementing
Typeof , so is discarding the evar_map a safe choice there?
TypeOf which is then fed to the printer :)
A SerAPI query, now that you mention it, I could just look at what
Check is doing.
I think the question is: do you want this call to be stateless? If so, protect the vernac state
Check ltac:(abstract tt) is pure because the STM says so, not because it actually is.
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