summaryrefslogtreecommitdiff
path: root/src/pretty_print_coq.ml
AgeCommit message (Expand)Author
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-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-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-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-08Add parameterization support for bitfields.Prashanth Mundkur
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
2018-12-29Coq: ensure that recursive functions computeBrian Campbell
2018-12-27Coq: avoid putting ambiguous numeric literals in Coq outputBrian Campbell
2018-12-27Coq: fix name clashes and instantiation calculationBrian Campbell
2018-12-26More cleanupAlasdair Armstrong
2018-12-26Some cleanupAlasdair Armstrong
2018-12-22Improve error messages and debuggingAlasdair Armstrong
2018-12-20Fix monomorpisation tests with typechecker changesAlasdair Armstrong
2018-12-19Coq: handle pairs of ranges (and other existential types) properlyBrian Campbell
2018-12-19Coq: handle existentials in hypotheses during solving, add max_nat, better castsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 04:45:53 +0000