aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/native/structures.ml
Commit message (Expand)AuthorAgeFilesLines
* Update copyrightChantal Keller2021-05-261-1/+1
* Properly check veriT exit code and warnings (#48)ckeller2019-04-121-0/+1
* V8.9 (#43)ckeller2019-03-151-2/+2
* Support for native-coqChantal Keller2019-03-121-3/+8
* V8.8 (#42)ckeller2019-03-111-65/+90
* V8.7 (#36)ckeller2019-02-141-1/+16
* Merge from LFSC (#26)ckeller2019-01-281-9/+9
* Adding support for lemmas in the command veritQuentin Garchery2018-10-281-0/+6
* formattingQuentin Garchery2018-10-271-1/+1
* now compiles with standard coq (including 8.6.1 from opam)Valentin Blot2018-07-201-0/+4
* Compiles with both versions of CoqChantal Keller2017-10-031-0/+7
* Hopefully solved the problem with universes for the tacticChantal Keller2016-09-281-0/+2
* Uniform treatment of sat and smt tacticsChantal Keller2016-09-281-2/+1
* Improved performance with coq-8.5Chantal Keller2016-09-281-1/+1
* More modularity on the format of traces depending on the version of coqChantal Keller2016-09-231-0/+28
* 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/+8
* Updating of the copyrightChantal Keller2016-04-271-2/+2
* Both native-coq and Coq 8.5 are fully supportedChantal Keller2016-04-261-1/+11
* Make the tactic available for 8.5Chantal Keller2016-04-261-0/+2
* Light port to Coq 8.5 under progressChantal Keller2016-03-181-0/+72
* Removed old port to Coq 8.4Chantal Keller2016-03-021-55/+0
* Corrected a bug introduced in native compilationChantal Keller2015-02-121-1/+2
* More on the support for standard Coq (not working yet)Chantal Keller2015-02-101-0/+6
* 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-131-0/+26
generated by cgit (git 2.34.1) at 2024-07-02 22:21:54 +0000