summaryrefslogtreecommitdiff
path: root/lib/coq/Hoare.v
AgeCommit message (Expand)Author
2020-08-26Coq: replace other uses of omega with liaBrian Campbell
2020-06-10Prepare Coq library for packagingBrian Campbell
2020-01-07Coq: accelerate wp steps by improving application of existing specsBrian Campbell
2019-12-19Coq library improvementsBrian Campbell
2019-11-29Coq: switch to boolean predicates for Sail-type propertiesBrian Campbell
2019-11-13Coq: more proof supportBrian Campbell
2019-09-19Change Coq Hoare logic rules to produce nicer preconditionsBrian Campbell
2019-09-19Expand Coq Hoare logic and congruence rules to more operatorsBrian Campbell
2019-08-22Coq: tactics to do rewrites under state monad, simple wp computationBrian Campbell
2019-07-31Coq: tweak Hoare proofs a littleBrian Campbell
2019-07-31Coq: reasoning for until loopsBrian Campbell
2019-07-25Basic port of proof machinery to CoqBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 16:00:47 +0000