summaryrefslogtreecommitdiff
path: root/lib/coq/Sail2_prompt.v
AgeCommit message (Expand)Author
2020-06-10Prepare Coq library for packagingBrian Campbell
2019-11-29Coq: switch to boolean predicates for Sail-type propertiesBrian Campbell
2019-10-24Coq: use `abstract` to separate out proofs from definitionsBrian Campbell
2019-09-19Expand Coq Hoare logic and congruence rules to more operatorsBrian Campbell
2019-08-19Coq: add bools_of_bits_nondet and friends to libraryBrian Campbell
2019-07-31Coq: reasoning for until loopsBrian Campbell
2019-07-25Basic port of proof machinery to CoqBrian Campbell
2019-05-19Coq: proper definitions for some undefined value functionsBrian Campbell
2019-04-15Basic loop termination measures for CoqBrian Campbell
2019-04-05Coq: termination measures for mutually recursive functionsBrian Campbell
2019-02-28Coq: remove unused library definitionsBrian Campbell
2019-02-28Coq: Clean up rich boolean handling in backendBrian Campbell
2019-02-28Coq: more for informative booleansBrian Campbell
2019-02-28Coq: some work on bool simplificationBrian Campbell
2018-12-29Coq: ensure that recursive functions computeBrian Campbell
2018-12-12Move much of recursive function termination to a rewriteBrian Campbell
2018-12-11Initial attempt at using termination measures in CoqBrian Campbell
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:53:57 +0000