summaryrefslogtreecommitdiff
path: root/src/pretty_print_coq.ml
AgeCommit message (Expand)Author
2019-05-24Coq: support if-then-throw typechecking special caseBrian Campbell
2019-05-23Coq: support loops which update richly typed variablesBrian Campbell
2019-05-22Coq: replace inferrable integer arguments with _ at more typesBrian Campbell
2019-05-21Coq: introduce autocasts at variablesBrian Campbell
2019-05-20Coq: add some missing autocasts, avoid unnecessary patterns in letsBrian Campbell
2019-05-19Coq: remove unhelpful type printing restriction on early returnsBrian Campbell
2019-05-14Merge branch 'smt_experiments' into sail2Alasdair Armstrong
2019-05-14Add feature that allows functions to require type variables are constantAlasdair Armstrong
2019-05-13Parse dereferences in orderinary expressionsAlasdair
2019-04-19Coq: when replacing n_constraints in types allow for some rearrangementBrian Campbell
2019-04-17Coq: support pure loops with termination measuresBrian Campbell
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 03:00:40 +0000