aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests/Tests_verit.v
Commit message (Expand)AuthorAgeFilesLines
* Separate unit tests into vernac and tacticsChantal Keller2019-04-121-1445/+0
* Error message to state that tactics are not supported with native-coq (#47)ckeller2019-04-121-1/+1
* V8.7 (#36)ckeller2019-02-141-40/+14
* Cleaning (#35)QGarchery2019-02-121-6/+138
* tactic notations (#31)QGarchery2019-02-081-30/+30
* Fix passing the goal strongly hashed (in ra' rf') instead of normal goal (has...QGarchery2019-02-071-13/+13
* Merge from LFSC (#26)ckeller2019-01-281-45/+94
* 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-281-0/+352
* formattingQuentin Garchery2018-10-271-18/+17
* Zeq_bool -> Z.eqbQuentin Garchery2018-10-271-14/+14
* Tests for Coq-8.6Chantal Keller2017-10-031-0/+2
* Hopefully solved the problem with universes for the tacticChantal Keller2016-09-281-0/+17
* Correct parsing of <-> for veriTChantal Keller2016-05-021-0/+6
* Holes in proof:Chantal Keller2016-04-301-0/+37
* 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-261-3/+3
* 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-241-0/+13
* New targets [make vtest] and [make ztest] to perform unit tests for the vario...Chantal Keller2016-03-021-0/+862
generated by cgit (git 2.34.1) at 2024-06-29 09:10:12 +0000