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