summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-08-13Coq: more strings for RISC-VBrian Campbell
2018-08-13Coq: drop redundant final wildcard clausesBrian Campbell
2018-08-13Add constraints to RISC-V duopod, makefile rulesBrian Campbell
2018-08-13RISC-V: mult_range is ill-typed, use mult_atom insteadBrian Campbell
2018-08-13Guarded clauses rewrite: variable patterns subsume enumsBrian Campbell
2018-08-13Basic Coq support for RISC-VBrian Campbell
2018-08-13Coq: drop irrelevant definitions before constraint solvingBrian Campbell
2018-08-12Coq: handle enums in binders, make top-level patterns exhaustiveBrian Campbell
2018-08-10Coq: add some of string libraryBrian Campbell
2018-08-10Merge pull request #19 from Smattr/5DAF5338-94B5-4F7A-A1CB-1CBB72ED7E93Alasdair Armstrong
2018-08-09fix tutorial infix exampleMatthew Fernandez
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-09Coq: a bit more handling of unknown constraintsBrian 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-03Merge pull request #18 from Smattr/C756D3DD-F006-4132-A3E3-27856A697A25Alasdair Armstrong
2018-08-03Fix existential variable problems in monomorphisationBrian 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-02fix some typosMatthew Fernandez
2018-08-02Coq mips: fix deprecation warningBrian 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-02Coq: limit eauto to ensure termination in reasonable timeBrian Campbell
2018-08-02Fill in more Coq builtins for aarch64Brian Campbell
2018-08-02Update a few prover gitignoresBrian Campbell
2018-08-02Support for comment commands in emacs modeBrian Campbell
2018-08-02Merge pull request #17 from hirataqdees/patch-1Alasdair Armstrong
2018-08-01Coq: implicit range conversions for function arguments, debug tracingBrian Campbell
2018-07-31Add Coq names for more Aarch64 builtinsBrian Campbell
2018-07-28Update INSTALL.mdhirataqdees
2018-07-27Add some missing rv64i instructions, discovered when annotating the riscv isa...Prashanth Mundkur
2018-07-27Add a riscv latex target.Prashanth Mundkur
2018-07-27Remove unused U_effect constructorAlasdair Armstrong
2018-07-27Merge branch 'sail2' of github.com:rems-project/sail into sail2Peter Sewell
2018-07-27clean Makefile target to copy generated LaTeX to cheri-architecturePeter Sewell
2018-07-27Revert "wib" (mistaken delete of sail_latexcc)Peter Sewell
2018-07-27Make type annotations abstract in type_check.mliAlasdair Armstrong
2018-07-27wibPeter Sewell
2018-07-27Coq: remove out-of-date todo listBrian Campbell
2018-07-27Coq: patterns on bit literalsBrian Campbell
2018-07-27Check in snapshot of cheri latexAlasdair Armstrong
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 15:13:43 +0000