summaryrefslogtreecommitdiff
path: root/src/pretty_print_coq.ml
AgeCommit message (Expand)Author
2018-10-11Change the function type in the ASTAlasdair
2018-09-24Coq: avoid variables called tt (the unit constant)Brian Campbell
2018-09-24Coq: add autocasts at monad returnsBrian Campbell
2018-09-19Coq: track changes elsewhereBrian Campbell
2018-09-17Coq: fix types in aarch64_extras undefined_vector and casts for argumentsBrian Campbell
2018-09-17Coq: solve some constraint/type errors with AArch64Brian Campbell
2018-09-17Coq: remove an obsolete specialisationBrian Campbell
2018-09-13Coq: real built-ins for AArch64Brian Campbell
2018-09-12Coq: fix type annotations for early returnBrian Campbell
2018-09-12Coq: avoid some use of pattern binders to help Coq's type checkerBrian Campbell
2018-09-12Coq: print more type information for existentially typed vectorsBrian Campbell
2018-09-11Coq: some basic handling for more existentialsBrian Campbell
2018-09-11Coq: remove a bunch of Lem-ismsBrian Campbell
2018-09-04Coq: fix early returns with rich typesBrian Campbell
2018-09-03Coq: get top-level value definitions to work nicely againBrian Campbell
2018-09-03Coq: rework generation of dependent pairs so that they are onlyBrian Campbell
2018-08-31fix some compiler warningsJon French
2018-08-28fix some compiler not-matched warnings about Typ_bidir and Typ_internal_unknownJon French
2018-08-28add __POS__ argument to Err_unreachable for better error reportingJon French
2018-08-17Coq: also introduce autocast at type annotationsBrian Campbell
2018-08-16Add the type an expression was checked against to tannots, and use for CoqBrian Campbell
2018-08-15Get RISC-V on Coq into reasonable state to showBrian Campbell
2018-08-12Coq: handle enums in binders, make top-level patterns exhaustiveBrian 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-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-27Make type annotations abstract in type_check.mliAlasdair Armstrong
2018-07-27Coq: remove out-of-date todo listBrian Campbell
2018-07-25Remove unused internal AST nodesAlasdair Armstrong
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-13Coq: avoid a couple of common identifiersBrian Campbell
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-09Coq: remove some unnecessary castsBrian Campbell
2018-07-07Coq: precise generic vectorsBrian Campbell
2018-07-07Coq: supply index constraint in for loopsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 21:00:28 +0000