summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-08-12Coq: handle enums in binders, make top-level patterns exhaustiveBrian Campbell
2018-08-10Coq: add some of string libraryBrian Campbell
2018-08-09Coq: debugging on top-level letsBrian Campbell
2018-08-09Coq: tidy up debugging messagesBrian Campbell
2018-08-09Coq: decompose dependent pairs at internal_plet as well as letBrian Campbell
2018-08-09Coq: handle nats like ranges, not atomsBrian Campbell
2018-08-07Revert "Warnings: deal with all the deprecation warnings"Alasdair Armstrong
2018-08-07Lem: print more bitvector typesBrian Campbell
2018-08-07Fix propagation of overly-specific types in early_return rewriteBrian Campbell
2018-08-07Improve cast introduction for LemBrian Campbell
2018-08-03Fix existential variable problems in monomorphisationBrian Campbell
2018-08-03Coq: generalise dependent pair handling a littleBrian Campbell
2018-08-02Coq: remove type removal holdover from Lem backend, add MIPS lemmaBrian Campbell
2018-08-02Coq: proper precedence for constraints (both prop and bool)Brian Campbell
2018-08-01Coq: implicit range conversions for function arguments, debug tracingBrian Campbell
2018-07-27Remove unused U_effect constructorAlasdair Armstrong
2018-07-27Make type annotations abstract in type_check.mliAlasdair Armstrong
2018-07-27Coq: remove out-of-date todo listBrian Campbell
2018-07-27Coq: patterns on bit literalsBrian Campbell
2018-07-26Some tweaks to not and or patternsAlasdair Armstrong
2018-07-26Patterns: add or and not patternsAlastair Reid
2018-07-26Warnings: deal with all the deprecation warningsAlastair Reid
2018-07-25Remove unused internal AST nodesAlasdair Armstrong
2018-07-24Merge branch 'c_fixes' into sail2Alasdair Armstrong
2018-07-24Merge remote-tracking branch 'origin/sail2' into c_fixesAlasdair Armstrong
2018-07-24Move monomorphisation after mapping rewritesBrian Campbell
2018-07-24Now builds mips spec again.Alasdair
2018-07-23Coq: make all pattern matches in the output exhaustiveBrian Campbell
2018-07-17Coq: support effectful function signatures in axiom generationBrian Campbell
2018-07-17Coq: support returning rich integer types from effectful functionsBrian Campbell
2018-07-17Coq: handle E_constraint properlyBrian Campbell
2018-07-16Coq: fix false existential problemBrian Campbell
2018-07-16Coq: we also unfold lengthBrian Campbell
2018-07-16Coq: handle simple type variable matches properly and nat typeBrian Campbell
2018-07-16Coq: add support for more complex atom typesBrian Campbell
2018-07-13Merge branch 'sail2' of github.com:rems-project/sail into sail2Brian Campbell
2018-07-13Coq: avoid a couple of common identifiersBrian Campbell
2018-07-12Handle failures during interpreting betterAlasdair Armstrong
2018-07-12update arm and mips models for new type of write_ram builtin. Also fix c and ...Robert Norton
2018-07-12Coq: get rid of syntax error on exception handlingBrian Campbell
2018-07-12Coq: handle all bool conjunctions/disjunctionsBrian Campbell
2018-07-12Coq: more autocast insertionBrian Campbell
2018-07-12Coq: tuple matching in loopsBrian Campbell
2018-07-12Coq: more accurate autocast insertionBrian Campbell
2018-07-12Fix bug for large integers in OCaml compilationAlasdair Armstrong
2018-07-12Minor fix to support OCaml 4.02.3Shaked Flur
2018-07-12Fixes for ARM Sail tests, and get_time_ns for interpreterAlasdair
2018-07-11RISC-V model fixes for RMEMJon French
2018-07-11Partially revert change to add_vec_int et alThomas Bauereiss
2018-07-11Fix some signedness bugsThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:34:13 +0000