summaryrefslogtreecommitdiff
path: root/src/pretty_print_coq.ml
AgeCommit message (Expand)Author
2019-04-16Coq: don't record assertions in the context if Sail doesn'tBrian Campbell
2019-04-15Merge branch 'sail2' of github.com:rems-project/sail into sail2Jon French
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
2019-04-15Basic loop termination measures for CoqBrian Campbell
2019-04-06Various bugfixes and improvementsAlasdair
2019-04-05Coq: termination measures for mutually recursive functionsBrian Campbell
2019-04-05Coq: add missing effectful existential unpacking caseBrian Campbell
2019-04-04Coq: correct projection in plain monadic and/orBrian Campbell
2019-04-02Coq: replace n_constraints with equivalent bool variablesBrian Campbell
2019-03-21Coq: fix bug when multiple type variables map to the same identifierBrian Campbell
2019-03-20Coq: do more (and more uniform) simplificationBrian Campbell
2019-03-20Coq: be more careful about merging Sail variables and type variablesBrian Campbell
2019-03-19Coq: simplify away more trivial boolsBrian Campbell
2019-03-19Coq: more test workBrian Campbell
2019-03-19Coq: more work on testsBrian Campbell
2019-03-18Coq: get axiom generation to merge bool tyvars with argumentsBrian Campbell
2019-03-15Coq: some progress on the test suiteBrian Campbell
2019-03-15Coq: better loop handling, discharge some related proof obligationsBrian Campbell
2019-03-14Merge branch 'sail2' into rmem_interpreterJon French
2019-03-12Coq: fix parametrized record typesBrian Campbell
2019-03-12Coq: fix some boolean issues seen in armBrian Campbell
2019-03-11Improve ocamldoc commentsAlasdair Armstrong
2019-03-05Coq: use more local type information when constructing tuplesBrian Campbell
2019-03-05Coq: some debugging messagesBrian Campbell
2019-03-05Coq: output type-level Int definitionsBrian Campbell
2019-03-04Merge branch 'sail2' into rmem_interpreterJon French
2019-03-01Coq: some library compatibility changesBrian Campbell
2019-03-01Coq tidying: remove old definition, complete a pattern matchBrian Campbell
2019-03-01Coq: make iff `iff`Brian Campbell
2019-02-28Coq: Clean up rich boolean handling in backendBrian Campbell
2019-02-28Coq: more for informative booleansBrian Campbell
2019-02-28Coq: update tyvar merge information at other bindersBrian Campbell
2019-02-28Turn off some debugging messagesBrian Campbell
2019-02-28Coq: merge tyvars with corresponding variablesBrian Campbell
2019-02-28Coq: strip informative bools back to more uniform typesBrian Campbell
2019-02-28Coq: some work on bool simplificationBrian Campbell
2019-02-25Merge branch 'sail2' into rmem_interpreterJon French
2019-02-19Refactor specializationAlasdair Armstrong
2019-02-15Tweak intermediate language names for loop combinators to allow reparsingBrian Campbell
2019-02-15Coq: Partial simplification of rich bool typesBrian Campbell
2019-02-14Coq: special case printing of bind-if-then-else trees for decodingBrian Campbell
2019-02-13Merge branch 'sail2' into rmem_interpreterJon French
2019-02-08Add parameterization support for bitfields.Prashanth Mundkur
2019-02-03Merge branch 'sail2' into rmem_interpreterJon French
2019-01-25Coq: add enough to generate some output for arm-v8.5-aBrian Campbell
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
2019-01-14Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-11Updates for sail-arm releaseAlasdair Armstrong
2019-01-09Coq: the division used in smt.sail should be EuclideanBrian Campbell
2019-01-09Coq: add parens around negative integer literalsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 18:01:04 +0000