aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/standard
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 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-281-0/+6
* Uniform treatment of sat and smt tacticsChantal Keller2016-09-282-4/+3
* Improved performance with coq-8.5Chantal Keller2016-09-281-2/+2
* 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-234-6/+60
* Now, Coq 8.5 is the defaultChantal Keller2016-05-013-10/+69
* Print warnings when checking proofs with holesChantal Keller2016-04-301-0/+5
* Bring back the nice printing of automatically generated theoremsChantal Keller2016-04-301-1/+15
* Holes in proof:Chantal Keller2016-04-302-7/+57
* Updating of the copyrightChantal Keller2016-04-2710-52/+89
* Both native-coq and Coq 8.5 are fully supportedChantal Keller2016-04-261-1/+13
* Make the tactic available for 8.5Chantal Keller2016-04-261-0/+2
* - 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-1812-0/+7559
* Removed old port to Coq 8.4Chantal Keller2016-03-0212-7386/+0
* 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-107-61/+106
* 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
generated by cgit (git 2.34.1) at 2024-07-03 12:28:42 +0000