aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests
Commit message (Expand)AuthorAgeFilesLines
...
* Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-232-27/+218
* Reify polymorphic termsckeller2021-01-051-0/+10
* Testing BV subtractionChantal Keller2020-07-201-0/+16
* Close #10Chantal Keller2020-05-151-0/+18
* Test asynchronous and make the selected lemmas persistant (#66)ckeller2020-03-264-202/+246
* make test does not need cleaning anymoreChantal Keller2020-03-251-2/+6
* Add the full example of the webpage in the unit testsChantal Keller2020-01-161-0/+30
* Separate unit tests into vernac and tacticsChantal Keller2019-04-126-533/+580
* Error message to state that tactics are not supported with native-coq (#47)ckeller2019-04-121-1/+1
* V8.7 (#36)ckeller2019-02-142-40/+16
* Cleaning (#35)QGarchery2019-02-122-7/+139
* equalities on array and bv types (#34)QGarchery2019-02-121-11/+9
* tactic notations (#31)QGarchery2019-02-081-30/+30
* PR #28 solves some problems in the tests of the "smt" tacticsChantal Keller2019-02-071-14/+12
* Fix passing the goal strongly hashed (in ra' rf') instead of normal goal (has...QGarchery2019-02-072-13/+86
* Revisited example from CompCertChantal Keller2019-02-071-0/+7
* Merge from LFSC (#26)ckeller2019-01-2814-47/+1400
* verit also works when it doesn't use the conclusion (#24)QGarchery2018-12-031-2/+8
* Adding support for lemmas in the command veritQuentin Garchery2018-10-282-0/+362
* formattingQuentin Garchery2018-10-271-18/+17
* Zeq_bool -> Z.eqbQuentin Garchery2018-10-271-14/+14
* Tests for Coq-8.6Chantal Keller2017-10-032-0/+4
* Hopefully solved the problem with universes for the tacticChantal Keller2016-09-282-0/+27
* Correct parsing of <-> for veriTChantal Keller2016-05-021-0/+6
* Bring back the nice printing of automatically generated theoremsChantal Keller2016-04-301-1/+0
* Holes in proof:Chantal Keller2016-04-302-1/+38
* Possibility to embed any Coq proof in certificates (not tested yet)Chantal Keller2016-04-291-30/+30
* Both native-coq and Coq 8.5 are fully supportedChantal Keller2016-04-261-18/+14
* English commentsChantal Keller2016-04-262-5/+5
* Compatibility with native-coqChantal Keller2016-04-261-8/+8
* - Solved the Coq 8.5 problem relating to declaring section variablesChantal Keller2016-04-261-3/+3
* The simplest test for SMTChantal Keller2016-04-242-0/+17
* Port to 8.5: how to deal with universe constraintsChantal Keller2016-03-231-5/+0
* Light port to Coq 8.5 under progressChantal Keller2016-03-181-0/+5
* New targets [make vtest] and [make ztest] to perform unit tests for the vario...Chantal Keller2016-03-023-423/+427
* The current version of SMTCoq does not support SMTLIB "let" anymoreChantal Keller2016-03-021-0/+6
* All tests (but large benchmarks) succeedChantal Keller2015-02-111-7/+6
* Unit test for double negationChantal Keller2015-01-121-0/+4
* "let" testsv1.2Chantal Keller2015-01-121-21/+21
* Initial import of SMTCoq v1.2Chantal Keller2015-01-1243-0/+23483
generated by cgit (git 2.34.1) at 2024-05-18 19:36:28 +0000