[coq-platform] Smoke test broken about riscv-coq HOT 3 OPEN

This breakage concerns the 8.192024.01+beta1 pick

from riscv-coq.

I used the src/riscv/Examples/Fib.v file. If this is alright could you please close this issue ?

from riscv-coq.

I used the src/riscv/Examples/Fib.v file. If this is alright could you please close this issue ?

That looks like a good "smoke test" to me (even though I don't know anything specific about requirements on smoke tests in the coq platform). One thing to note is that this file doesn't need anything of the src/riscv/Proofs/ directory, if that is desired, src/riscv/Proofs/DecodeEncode.v could be used, but that one doesn't need anything from the src/riscv/Platform/ directory.

from riscv-coq.