summaryrefslogtreecommitdiff
path: root/lib/coq/Sail2_prompt.v
AgeCommit message (Expand)Author
2018-09-11Coq: some basic handling for more existentialsBrian Campbell
2018-09-06Coq: fill in a few more RISC-V axiomsBrian Campbell
2018-09-06Coq: fix up some barrier/memory definitions for RISC-VBrian Campbell
2018-09-03Coq: rework generation of dependent pairs so that they are onlyBrian Campbell
2018-08-03Coq: generalise dependent pair handling a littleBrian Campbell
2018-07-12Coq: remove unnecessary constraint on foreach loopsBrian Campbell
2018-07-07Coq: supply index constraint in for loopsBrian Campbell
2018-06-22Coq: library updates, esp extending bitvector multiplies, UndefinedBrian Campbell
2018-06-19Coq: library name update (as we did for Lem)Brian Campbell