summaryrefslogtreecommitdiff
path: root/riscv/coq.patch
AgeCommit message (Expand)Author
2018-09-05Coq: fill in trivial ranges in constraint solverBrian Campbell
2018-09-04Add a rewrite to minimise the number of functions marked as recursiveBrian Campbell
2018-09-03Coq: solver should split earlierBrian Campbell
2018-09-03Coq: update RISC-V patch againBrian Campbell
2018-09-03Coq: rework generation of dependent pairs so that they are onlyBrian Campbell
2018-08-16Add the type an expression was checked against to tannots, and use for CoqBrian Campbell
2018-08-15Get RISC-V on Coq into reasonable state to showBrian Campbell