summaryrefslogtreecommitdiff
path: root/lib/coq
AgeCommit message (Expand)Author
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
2019-01-22Don't hardcode location of BBV libraryThomas Bauereiss
2019-01-09Coq: the division used in smt.sail should be EuclideanBrian Campbell
2019-01-09Coq: add truncateLSB and import Zeuclid by defaultBrian Campbell
2019-01-01Coq: update instr_kinds from LemBrian Campbell
2018-12-29Coq: ensure that recursive functions computeBrian Campbell
2018-12-27Coq: make solver try hints before stripping away existentialsBrian Campbell
2018-12-19Coq: add zeros library function (used by MIPS)Brian Campbell
2018-12-19Coq: handle existentials in hypotheses during solving, add max_nat, better castsBrian Campbell
2018-12-17Adapt Coq and termination measure support to typechecker changesBrian 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-11-21Coq: min_natBrian Campbell
2018-11-21Coq: add equality for records and polymorphic vectorsBrian Campbell
2018-11-20Minor coq updatesBrian Campbell
2018-10-22Update Coq patch for RISC-V, add string_take to Coq libraryBrian Campbell
2018-09-19Coq: track changes elsewhereBrian Campbell
2018-09-19Coq: more fixes for AArch64Brian Campbell
2018-09-17Coq: solve some constraint/type errors with AArch64Brian Campbell
2018-09-17Coq: make generic_neq work on realBrian Campbell
2018-09-13Coq: real built-ins for AArch64Brian Campbell
2018-09-12Coq: make generic_eq work on more typesBrian Campbell
2018-09-12Coq: remove extra "True"s from constraintsBrian 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: more string handlingBrian Campbell
2018-09-06Coq: fix up some barrier/memory definitions for RISC-VBrian Campbell
2018-09-05Coq: fill in trivial ranges in constraint solverBrian Campbell
2018-09-03Coq: solver should split earlierBrian Campbell
2018-09-03Coq: get top-level value definitions to work nicely againBrian Campbell
2018-09-03Coq: rework generation of dependent pairs so that they are onlyBrian Campbell
2018-08-30Coq: correct endianness reversal bugBrian Campbell
2018-08-28Coq: make some library definitions computeBrian Campbell
2018-08-15Get RISC-V on Coq into reasonable state to showBrian Campbell
2018-08-14Coq: attempt a quick proof before an indepth oneBrian Campbell
2018-08-13Coq: more strings for RISC-VBrian Campbell
2018-08-13Coq: drop irrelevant definitions before constraint solvingBrian Campbell
2018-08-10Coq: add some of string libraryBrian Campbell
2018-08-09Coq: a bit more handling of unknown constraintsBrian Campbell
2018-08-03Coq: use a dummy constraint when the real one is unknownBrian Campbell
2018-08-03Coq: generalise dependent pair handling a littleBrian Campbell
2018-08-02Coq: limit eauto to ensure termination in reasonable timeBrian Campbell
2018-08-02Fill in more Coq builtins for aarch64Brian Campbell
2018-08-01Coq: implicit range conversions for function arguments, debug tracingBrian Campbell
2018-07-18Coq: constraint solving improvementsBrian Campbell
2018-07-17Coq: integer shiftsBrian Campbell
2018-07-17Coq: add printing stubsBrian Campbell
2018-07-17Coq: handle E_constraint properlyBrian Campbell
2018-07-16Coq: add support for more complex atom typesBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 18:47:43 +0000