search

mit-plv / riscv-coq

RISC-V Specification in Coq
BSD 3-Clause "New" or "Revised" License
109 stars 17 forks source link

ExtSpec for FE310 #23

Closed joonwonc closed 5 years ago

joonwonc commented 5 years ago

This code is exactly the one from https://github.com/mit-plv/bedrock2/blob/master/compiler/src/compilerExamples/MMIO.v#L122

The bedrock2 repository will have another pull request that includes this change and the ExtSpec definition being removed from the original place (and some more appropriate changes).

joonwonc commented 5 years ago

I made all the suggested changes from @samuelgruetter and got compilation green. I will merge this to master tonight unless someone suggests something else.