aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtCommands.ml
Commit message (Expand)AuthorAgeFilesLines
* Print warnings when checking proofs with holesChantal Keller2016-04-301-5/+27
* Bring back the nice printing of automatically generated theoremsChantal Keller2016-04-301-8/+8
* Solved the efficiency problemChantal Keller2016-04-301-34/+83
* Holes in proof:Chantal Keller2016-04-301-6/+22
* Possibility to embed any Coq proof in certificates (not tested yet)Chantal Keller2016-04-291-67/+70
* Updating of the copyrightChantal Keller2016-04-271-0/+16
* Both native-coq and Coq 8.5 are fully supportedChantal Keller2016-04-261-6/+5
* Compatibility with native-coqChantal Keller2016-04-261-5/+5
* Tactic verit for 8.5Chantal Keller2016-04-261-4/+4
* Light port to Coq 8.5 under progressChantal Keller2016-03-181-4/+4
* Code refactoringChantal Keller2016-03-021-0/+256