Robbert Krebbers

Ah, no, it would not. By doing: ``` ptr_eq x y (fun _ _ => true) (fun _ => false) ``` We end up with the same problem we had...

Any idea how to do that, without having to delete my repository and merging it somehow with a new fork?

Thanks for this! With regard to your question, Coq has issues automatically infering the `Decision` instance for `frozen`. In a previous PR, you hacked around that using an `unfold` and...

> Having `ASPM_BATTERY_POLICY` and `ASPM_AC_POLICY` configuration variables would be ideal for me I second that it would be great to have these options. With my laptop I ran into the...

Like Ralf I am also excited about this! Great Job to the VST team!

I would still be very happy to see more of the evarconv heuristics being ported to unification.ml./

I don't follow the Coq Gitter, so can you remind us what this discussion was about exactly? And what do you mean by compatible?

> In stdpp it appears you need to find a concrete implementation of a map with your key (Zmap, Nmap, etc.) which is much less discoverable. The map implementation that...

This is very minor, so let's do this after the artifact evaluation to avoid confusion with different project names.