aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
...
* 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
|
* Hopefully solved the problem with universes for the tacticChantal Keller2016-09-284-25/+83
|
* 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
|
* Correct parsing of <-> for veriTChantal Keller2016-05-021-0/+2
|
* Now, Coq 8.5 is the defaultChantal Keller2016-05-019-460/+83
|
* Print warnings when checking proofs with holesChantal Keller2016-04-305-24/+46
|
* Bring back the nice printing of automatically generated theoremsChantal Keller2016-04-304-13/+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-3016-33/+233
| | | | | | | - can now take learned clauses as argument - returns a whole clause (and not only a literal) - tested for the vernacular commands Warning: seems to slow down 8.5 version
* Possibility to embed any Coq proof in certificates (not tested yet)Chantal Keller2016-04-296-185/+169
|
* 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-2610-23/+77
|
* Compatibility with native-coqChantal Keller2016-04-263-15/+15
|
* 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-262-10/+10
| | | | - Correct equality check of atoms and formulas for processing congruence closure
* Port to 8.5: how to deal with universe constraintsChantal Keller2016-03-231-3/+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-1827-36/+8071
|
* 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 ↵Chantal Keller2016-03-022-1/+11
| | | | various solvers separately
* Corrected a bug in the generation of certificates for CNF computation of iffChantal Keller2015-06-181-1/+1
|
* 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
|
* Corrected a bug introduced in native compilationChantal Keller2015-02-121-1/+2
|
* 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 ↵Chantal Keller2015-02-111-2/+7
| | | | (the last element is the default)
* 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 ↵Chantal Keller2015-01-135-75/+42
| | | | standard coq
* 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
|
* Initial import of SMTCoq v1.2Chantal Keller2015-01-1250-0/+24014
generated by cgit (git 2.34.1) at 2024-07-01 12:12:27 +0000