aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-061-0/+22
|\
| * Another silent change of veriT...Chantal Keller2021-05-061-0/+22
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-061-0/+12
|\|
| * Example for #92Chantal Keller2021-05-061-0/+12
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-051-0/+35
|\|
| * CompDec on interpreted typeChantal Keller2021-05-051-0/+35
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-051-0/+31
|\|
| * Reify applied polymorphic terms with compdecChantal Keller2021-05-051-0/+31
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-281-0/+14
|\|
| * Solve a bug when reifying under a binderChantal Keller2021-04-281-0/+14
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-261-0/+11
|\|
| * Equality between Booleans should be changed for hypothesesChantal Keller2021-04-261-0/+11
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-261-4/+13
|\|
| * CompDec are automatically discharged when generated by the OCaml tactic, when...Chantal Keller2021-04-261-4/+13
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-262-57/+51
|\|
| * Take hypotheses from the local context (#91)ckeller2021-04-262-57/+51
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-212-40/+173
|\|
| * Convert hypotheses from Prop to bool (#89)ckeller2021-04-212-40/+173
* | Batch parallelismChantal Keller2021-02-231-1/+1
|/
* Example of groups in unit testsChantal Keller2021-02-231-18/+37
* The examples on lists uses the true list typeChantal Keller2021-02-231-10/+5
* 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
generated by cgit (git 2.34.1) at 2024-05-20 11:34:03 +0000