summaryrefslogtreecommitdiff
path: root/lib/coq/Sail2_operators_mwords.v
AgeCommit message (Expand)Author
2020-06-10Prepare Coq library for packagingBrian Campbell
2020-02-05Tweak Coq scopes for 8.11Brian Campbell
2019-12-19Coq library improvementsBrian Campbell
2019-12-06Coq: use proof irrelevance for a few propertiesBrian 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-02Coq: add properly checked subrange update, reduce importsBrian Campbell
2019-08-13Coq: definitions for cheri128 modelBrian Campbell
2019-06-27Coq: less constrained version of slice for ARM modelBrian Campbell
2019-05-24Coq: switch to computable versions of BBV shiftsBrian Campbell
2019-05-19Coq: add signed bitvector to integer function that doesn't need >0 constraintBrian Campbell
2019-04-16Coq: set_slice typoBrian Campbell
2019-03-19Coq: more test workBrian Campbell
2019-01-09Coq: add truncateLSB and import Zeuclid by defaultBrian Campbell
2018-12-19Coq: add zeros library function (used by MIPS)Brian Campbell
2018-11-21Coq: add equality for records and polymorphic vectorsBrian Campbell
2018-11-20Minor coq updatesBrian Campbell
2018-09-19Coq: more fixes for AArch64Brian Campbell
2018-08-28Coq: make some library definitions computeBrian Campbell
2018-08-15Get RISC-V on Coq into reasonable state to showBrian Campbell
2018-07-02Coq: add some string functionsBrian Campbell
2018-06-25Coq: automatic cast introductionBrian Campbell
2018-06-22Precise bitvector subrange functions for Coq.Brian Campbell
2018-06-22Coq: library updates, esp extending bitvector multiplies, UndefinedBrian Campbell
2018-06-20Coq: reverse_endiannessBrian Campbell
2018-06-20Coq: a few more opsBrian 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-01-31 12:35:18 +0000