I'm getting a DestKO
here, indeed ty
is not an evar but Type
.
How is that possible?
let sigma, (ty, _) = Evarutil.new_type_evar ~naming:(...) env sigma Evd.univ_rigid in
let ty_key, _ = EConstr.destEvar sigma ty in
Is the original sigma
clean?
WDYM? It is not empty. But in any case, what would make the API misbehave so much? I cannot even see how it is possible for the API to not return an evar
By clean I mean it wasn't messed up with in a way that break invariants
It doesn't have to be empty, of course
by looking at it, it's not possible for the code to return a non-evar there, except maybe if you screwed up the fresh evar number generator
Pierre-Marie Pédrot said:
by looking at it, it's not possible for the code to return a non-evar there, except maybe if you screwed up the fresh evar number generator
Yeah this is what I had in mind, something in the initial conditions which makes the new evar already assigned to something.
Oh... I see, digging deeper
Last updated: May 28 2023 at 16:30 UTC