aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests/Tests_verit.v
Commit message (Expand)AuthorAgeFilesLines
* 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