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 :)
What is TypeOf
?
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
look at About
instead
eg 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