aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/standard/structures.ml
Commit message (Expand)AuthorAgeFilesLines
* getting rid of native-coq (#95)vblot2021-05-281-237/+0
* Get rid of most of our copy of micromega's source code (#94)vblot2021-05-281-4/+1
* Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-261-1/+1
|\
| * Update copyrightChantal Keller2021-05-261-1/+1
* | Compiles with Coq-8.10Chantal Keller2020-03-311-0/+1
* | Port to coq-8.10 under progressChantal Keller2020-03-311-13/+18
|/
* Properly check veriT exit code and warnings (#48)ckeller2019-04-121-0/+1
* V8.9 (#43)ckeller2019-03-151-8/+8
* V8.8 (#42)ckeller2019-03-111-90/+128
* V8.7 (#36)ckeller2019-02-141-24/+41
* CleanupChantal Keller2019-01-291-4/+0
* Merge from LFSC (#26)ckeller2019-01-281-12/+16
* Adding support for lemmas in the command veritQuentin Garchery2018-10-281-0/+9
* now compiles with standard coq (including 8.6.1 from opam)Valentin Blot2018-07-201-0/+3
* Compiles with both versions of CoqChantal Keller2017-10-031-0/+7
* Compiles with Coq-8.6Chantal Keller2017-10-031-5/+6
* (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-281-2/+1
* Improved performance with coq-8.5Chantal Keller2016-09-281-2/+2
* More modularity on the format of traces depending on the version of coqChantal Keller2016-09-231-0/+15
* 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
* Updating of the copyrightChantal Keller2016-04-271-2/+2
* 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
* Light port to Coq 8.5 under progressChantal Keller2016-03-181-0/+98
* Removed old port to Coq 8.4Chantal Keller2016-03-021-77/+0
* 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-101-7/+32
* Start porting to the standard version of Coq (not finished yet)Chantal Keller2015-01-131-0/+47