aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* 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
* OPAM currently not supportedChantal Keller2015-12-031-79/+31
* Corrected a bug in the generation of certificates for CNF computation of iffChantal Keller2015-06-181-1/+1
* More details on the installation of the proversChantal Keller2015-04-301-1/+22
* More details on extractionChantal Keller2015-04-301-8/+10
* Generic program to run the extracted checkers (basic error messages)Chantal Keller2015-04-301-14/+18
* Generic program to run the extracted checkersChantal Keller2015-04-302-2/+48
* Corrections in the installation instructionsChantal Keller2015-02-141-3/+4
* Other corrections in the installation instructionsChantal Keller2015-02-141-3/+8
* Corrections in installation instructionsChantal Keller2015-02-141-3/+3
* New installation instructionsChantal Keller2015-02-141-5/+53
* Corrected a bug introduced in native compilationChantal Keller2015-02-121-1/+2
* All tests (but large benchmarks) succeedChantal Keller2015-02-111-7/+6
* Implemented cast on int31 directlyChantal Keller2015-02-113-61/+114
* COrrect implementation of foldi_cont and foldi_down_contChantal Keller2015-02-111-6/+6
* More efficient initialization of an arrayChantal Keller2015-02-111-7/+3
* Corrected a bug in the initialization of arrays for the standard version (the...Chantal Keller2015-02-111-2/+7
* More on the support for standard Coq (not working yet)Chantal Keller2015-02-1016-90/+139
* Frontend for the standard version of Coq (still bad computational behavior)Chantal Keller2015-02-1012-325/+3551
* Start porting to the standard version of Coq (not finished yet)Chantal Keller2015-01-1310-0/+4070
* Identify ML functions that are implemented differently in native-coq and in s...Chantal Keller2015-01-135-75/+42
* Identify ML functions that depend on native-coqChantal Keller2015-01-1312-41/+74
* Room for compilation with other versions of CoqChantal Keller2015-01-133-4/+10
generated by cgit (git 2.34.1) at 2024-06-29 09:54:48 +0000