aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions
Commit message (Expand)AuthorAgeFilesLines
...
* Compiles with Coq-8.6Chantal Keller2017-10-037-97/+245
* Some proofs for the Int63 glueChantal Keller2016-10-141-8/+104
* Some proofs for the Int63 glueChantal Keller2016-10-106-125/+192
* 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-071-2/+2
* (Hopefully) repared the universes problemsChantal Keller2016-10-071-1/+4
* Hopefully solved the problem with universes for the tacticChantal Keller2016-09-282-0/+8
* Uniform treatment of sat and smt tacticsChantal Keller2016-09-284-8/+6
* Improved performance with coq-8.5Chantal Keller2016-09-282-3/+3
* Use the most efficient operations of Int31Chantal Keller2016-09-282-47/+34
* Use the Int31 library with coq-8.5Chantal Keller2016-09-286-3141/+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-238-9/+132
* Now, Coq 8.5 is the defaultChantal Keller2016-05-016-18/+134
* Print warnings when checking proofs with holesChantal Keller2016-04-302-0/+10
* Bring back the nice printing of automatically generated theoremsChantal Keller2016-04-302-2/+23
* Holes in proof:Chantal Keller2016-04-304-9/+61
* Updating of the copyrightChantal Keller2016-04-2711-54/+91
* Both native-coq and Coq 8.5 are fully supportedChantal Keller2016-04-262-2/+24
* Make the tactic available for 8.5Chantal Keller2016-04-262-0/+4
* - Solved the Coq 8.5 problem relating to declaring section variablesChantal Keller2016-04-261-2/+2
* 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-1815-0/+8162
* Removed old port to Coq 8.4Chantal Keller2016-03-0215-7966/+0
* New targets [make vtest] and [make ztest] to perform unit tests for the vario...Chantal Keller2016-03-022-1/+11
* 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 (the...Chantal Keller2015-02-111-2/+7
* More on the support for standard Coq (not working yet)Chantal Keller2015-02-108-61/+112
* Frontend for the standard version of Coq (still bad computational behavior)Chantal Keller2015-02-1011-325/+3548
* Start porting to the standard version of Coq (not finished yet)Chantal Keller2015-01-139-0/+4064
* Identify ML functions that are implemented differently in native-coq and in s...Chantal Keller2015-01-131-3/+25
* Identify ML functions that depend on native-coqChantal Keller2015-01-133-0/+541
generated by cgit (git 2.34.1) at 2024-06-29 07:24:54 +0000