Enrico Tassi (Mar 03 2023 at 09:44): Enrico Tassi (Mar 03 2023 at 09:44):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?
Enrico Tassi (Mar 03 2023 at 09:48):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
Maxime Dénès (Mar 03 2023 at 09:48):By clean I mean it wasn't messed up with in a way that break invariants
Maxime Dénès (Mar 03 2023 at 09:49):It doesn't have to be empty, of course
Pierre-Marie Pédrot (Mar 03 2023 at 09:50):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
Maxime Dénès (Mar 03 2023 at 09:51):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.
Enrico Tassi (Mar 03 2023 at 09:53):Oh... I see, digging deeper
Last updated: Dec 05 2023 at 12:01 UTC