aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
...
* - auto-generated mli files for future documentationValentin Blot2017-11-2424-6/+1007
* Command to bypass typechecking when generating a zchaff theoremChantal Keller2017-11-143-2/+16
* Update extraction (only ml)Valentin Blot2017-11-063-3/+4
* Compiles with both versions of CoqChantal Keller2017-10-035-41/+55
* make install for Coq-8.6Chantal Keller2017-10-032-10/+4
* Tests for Coq-8.6Chantal Keller2017-10-032-6/+31
* 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
* 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
* 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
* 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
* 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 vario...Chantal Keller2016-03-022-1/+11
* 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
generated by cgit (git 2.34.1) at 2024-06-29 16:27:34 +0000