aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/native
Commit message (Expand)AuthorAgeFilesLines
* getting rid of native-coq (#95)vblot2021-05-287-1192/+0
* Get rid of most of our copy of micromega's source code (#94)vblot2021-05-282-4/+0
* Update copyrightChantal Keller2021-05-265-5/+5
* Made SmtCommands independent from VeritSyntaxChantal Keller2019-09-252-4/+8
* 3rdpartyChantal Keller2019-07-152-26/+30
* Separate unit tests into vernac and tacticsChantal Keller2019-04-122-11/+6
* Properly check veriT exit code and warnings (#48)ckeller2019-04-122-0/+2
* Error message to state that tactics are not supported with native-coq (#47)ckeller2019-04-124-6/+63
* V8.9 (#43)ckeller2019-03-152-5/+5
* Support for native-coqChantal Keller2019-03-122-9/+14
* V8.8 (#42)ckeller2019-03-112-109/+177
* V8.7 (#36)ckeller2019-02-142-3/+28
* Merge from LFSC (#26)ckeller2019-01-286-27/+180
* Adding support for lemmas in the command veritQuentin Garchery2018-10-283-1/+18
* New files SmtBtype.ml(i) for module formerly in SmtAtomQuentin Garchery2018-10-282-2/+6
* Updated Makefile instructionsQuentin Garchery2018-10-271-6/+9
* formattingQuentin Garchery2018-10-271-1/+1
* conversion tacticsValentin Blot2018-10-252-0/+2
* now compiles with standard coq (including 8.6.1 from opam)Valentin Blot2018-07-202-0/+5
* - auto-generated mli files for future documentationValentin Blot2017-11-243-2/+84
* Command to bypass typechecking when generating a zchaff theoremChantal Keller2017-11-141-0/+7
* Compiles with both versions of CoqChantal Keller2017-10-031-0/+7
* Corrected a bug with holes in proofs (for native-coq)Chantal Keller2016-10-071-2/+2
* Hopefully solved the problem with universes for the tacticChantal Keller2016-09-281-0/+2
* Uniform treatment of sat and smt tacticsChantal Keller2016-09-282-4/+3
* 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-234-3/+72
* Now, Coq 8.5 is the defaultChantal Keller2016-05-013-8/+65
* 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
* Holes in proof:Chantal Keller2016-04-302-2/+4
* 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-183-0/+603
* Removed old port to Coq 8.4Chantal Keller2016-03-023-580/+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
* 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-133-0/+541
generated by cgit (git 2.34.1) at 2024-06-26 14:33:48 +0000