It seems that fiat-crypto is broken on master, likely due to the last commit that was introduced to fix backwards compat.
cc @Jason Gross
Ugh, is there no way to write
instantiate (1:=...) in (value of H) which is compatible with both 8.9 and master?
Ok, I've pushed another commit that hopefully fixes things
Current Coq still allows Value but it triggers a warning, and it is seemingly fatal in the CI
Last updated: Oct 16 2021 at 07:02 UTC