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: Dec 07 2023 at 06:38 UTC