summaryrefslogtreecommitdiff
path: root/lib/coq
AgeCommit message (Expand)Author
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-02Coq: limit eauto to ensure termination in reasonable timeBrian Campbell
2018-08-02Fill in more Coq builtins for aarch64Brian Campbell
2018-08-01Coq: implicit range conversions for function arguments, debug tracingBrian Campbell
2018-07-18Coq: constraint solving improvementsBrian Campbell
2018-07-17Coq: integer shiftsBrian Campbell
2018-07-17Coq: add printing stubsBrian Campbell
2018-07-17Coq: handle E_constraint properlyBrian Campbell
2018-07-16Coq: add support for more complex atom typesBrian Campbell
2018-07-12Coq: handle all bool conjunctions/disjunctionsBrian Campbell
2018-07-12Coq: remove unnecessary constraint on foreach loopsBrian Campbell
2018-07-09Bits for bits of aarch64 in coqBrian Campbell
2018-07-07Coq: bbv have reorganised their repositoryBrian Campbell
2018-07-07Coq: precise generic vectorsBrian Campbell
2018-07-07Coq: supply index constraint in for loopsBrian Campbell
2018-07-07Coq: eq_range should take proofsBrian Campbell
2018-07-06Coq: use List.In predicates in constraint solving; make other bits robustBrian Campbell
2018-07-05Coq: get index_list rightBrian Campbell
2018-07-02Coq: add some string functionsBrian Campbell
2018-07-02Coq: replace simpl in a tactic with a more precise "change"Brian Campbell
2018-06-25Coq: add typeclass based comparison, and instantiate for enumsBrian Campbell
2018-06-25Coq: automatic cast introductionBrian Campbell
2018-06-22Precise bitvector subrange functions for Coq.Brian Campbell
2018-06-22Add coq builtins for MIPSBrian Campbell
2018-06-22Coq: library updates, esp extending bitvector multiplies, UndefinedBrian Campbell
2018-06-22Coq: project away range types in comparisonsBrian Campbell
2018-06-20Coq: reverse_endiannessBrian Campbell
2018-06-20Coq: Tidy up libraries, export StringBrian Campbell
2018-06-20Coq: a few more opsBrian Campbell
2018-06-19Coq: library name update (as we did for Lem)Brian Campbell
2018-06-18Separate bitvector access/update from generic vector access in std preludeBrian Campbell
2018-06-18Coq: update prompt monad wrt LemBrian Campbell
2018-06-13Coq: library updates, informative type errors, fix type aliasesBrian Campbell
2018-06-12Coq: support for range type, along with related existential improvementsBrian Campbell
2018-06-12Coq: add more to libraryBrian Campbell
2018-06-08Coq: existential and constraint solving workBrian Campbell
2018-06-08Coq: some very basic existential supportBrian Campbell
2018-05-25Coq: fill in some built-insBrian Campbell
2018-05-24Coq: solve more constraintsBrian Campbell
2018-05-24Help launch coqideBrian Campbell
2018-05-24Import (rather hacky) Coq Sail librariesBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:55:54 +0000