aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Removed unused fileChantal Keller2017-10-031-62/+0
* Compiles with Coq-8.6Chantal Keller2017-10-0314-151/+296
* Towards Coq 8.6Chantal Keller2017-10-022-10/+9
* New version of veriTChantal Keller2016-11-021-5/+13
* Allow premices of the transitivity rule to be reflexivity lemmasChantal Keller2016-11-021-8/+15
* Some proofs for the Int63 glueChantal Keller2016-10-141-8/+104
* Some proofs for the Int63 glueChantal Keller2016-10-107-126/+199
* Corrected a bug with holes in proofs (for native-coq)Chantal Keller2016-10-071-2/+2
* Corrected a bug with holes in proofsChantal Keller2016-10-074-15/+17
* (Hopefully) repared the universes problemsChantal Keller2016-10-071-1/+4
* Updated the installation instructionsChantal Keller2016-09-281-2/+2
* Hopefully solved the problem with universes for the tacticChantal Keller2016-09-286-25/+110
* Uniform treatment of sat and smt tacticsChantal Keller2016-09-285-14/+8
* Improved performance with coq-8.5Chantal Keller2016-09-284-24/+50
* Use the most efficient operations of Int31Chantal Keller2016-09-282-47/+34
* Use the Int31 library with coq-8.5Chantal Keller2016-09-287-3144/+0
* More straightforward definitions in Int63Native_standardChantal Keller2016-09-261-32/+32
* More modularity on the format of traces depending on the version of coqChantal Keller2016-09-2311-39/+166
* TypoChantal Keller2016-09-211-1/+1
* Correct parsing of <-> for veriTChantal Keller2016-05-022-0/+8
* Installation via opamChantal Keller2016-05-021-2/+23
* Example.v: new paths for Coq 8.5Chantal Keller2016-05-021-2/+5
* Now, Coq 8.5 is the defaultChantal Keller2016-05-0111-477/+119
* Print warnings when checking proofs with holesChantal Keller2016-04-305-24/+46
* Bring back the nice printing of automatically generated theoremsChantal Keller2016-04-305-14/+34
* Proved correctness of the checker for holesChantal Keller2016-04-301-14/+31
* Solved the efficiency problemChantal Keller2016-04-301-34/+83
* Holes in proof:Chantal Keller2016-04-3018-34/+271
* Possibility to embed any Coq proof in certificates (not tested yet)Chantal Keller2016-04-297-215/+199
* Updating of the copyrightChantal Keller2016-04-2756-122/+359
* The tactic "verit" generates more user-friendly subgoalsChantal Keller2016-04-263-22/+19
* Both native-coq and Coq 8.5 are fully supportedChantal Keller2016-04-2611-41/+91
* English commentsChantal Keller2016-04-262-5/+5
* Compatibility with native-coqChantal Keller2016-04-264-23/+23
* Tactic verit for 8.5Chantal Keller2016-04-261-4/+4
* Tactic zchaff for 8.5Chantal Keller2016-04-262-12/+20
* Make the tactic available for 8.5Chantal Keller2016-04-264-9/+13
* - Solved the Coq 8.5 problem relating to declaring section variablesChantal Keller2016-04-263-13/+13
* The simplest test for SMTChantal Keller2016-04-242-0/+17
* Port to 8.5: how to deal with universe constraintsChantal Keller2016-03-232-8/+7
* Solved a dependency problem for the compilation with Coq 8.5Chantal Keller2016-03-212-7/+4
* Light port to Coq 8.5 under progressChantal Keller2016-03-1828-36/+8076
* No more "configure.sh"Chantal Keller2016-03-021-1/+0
* Code refactoringChantal Keller2016-03-027-360/+304
* Separate verit input (smtlib2) from outputChantal Keller2016-03-027-16/+19
* Removed old port to Coq 8.4Chantal Keller2016-03-0216-7419/+6
* New targets [make vtest] and [make ztest] to perform unit tests for the vario...Chantal Keller2016-03-025-424/+438
* The current version of SMTCoq does not support SMTLIB "let" anymoreChantal Keller2016-03-021-0/+6
* Release 1.3Chantal Keller2016-03-011-3/+3
* Use a fork of native-coqv1.3Chantal Keller2015-12-071-2/+2
generated by cgit (git 2.34.1) at 2024-07-05 20:11:42 +0000