Stream: Coq devs & plugin devs

Topic: new_type_evar returning a non-evar


view this post on Zulip 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

view this post on Zulip Maxime Dénès (Mar 03 2023 at 09:46):

Is the original sigma clean?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Mar 03 2023 at 09:49):

It doesn't have to be empty, of course

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Mar 03 2023 at 09:53):

Oh... I see, digging deeper


Last updated: Dec 05 2023 at 12:01 UTC