summaryrefslogtreecommitdiff
path: root/lib/coq/Sail2_state_monad.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-09-19Expand Coq Hoare logic and congruence rules to more operatorsBrian Campbell
2019-08-14Coq library work for proofs:Brian Campbell
2019-07-25Basic port of proof machinery to CoqBrian Campbell
2019-04-10Coq: update prompt monad to match the Lem, and port the state monad/liftingBrian Campbell
2018-06-19Coq: library name update (as we did for Lem)Brian Campbell