aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions
Commit message (Expand)AuthorAgeFilesLines
* Better use of the typeclass mechanismChantal Keller2021-10-211-2/+2
* fix array notations clash with ssreflectvblot2021-08-251-0/+2
* The verit tactics now immediately fail if veriT is not installedChantal Keller2021-07-111-58/+63
* Update copyrightChantal Keller2021-05-2616-16/+16
* prop2bool_hyps insensitive to parenthesisChantal Keller2021-04-281-1/+1
* CompDec are automatically discharged when generated by the OCaml tactic, when...Chantal Keller2021-04-261-14/+17
* Take hypotheses from the local context (#91)ckeller2021-04-261-12/+115
* Convert hypotheses from Prop to bool (#89)ckeller2021-04-213-30/+15
* Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-231-6/+6
* Remove invalid axiom (see #71)Chantal Keller2020-06-291-1/+5
* Test asynchronous and make the selected lemmas persistant (#66)ckeller2020-03-262-5/+28
* make test does not need cleaning anymoreChantal Keller2020-03-251-4/+4
* Revert "Search correctly for `num` library (#60)" (#61)ckeller2020-02-271-4/+0
* Search correctly for `num` library (#60)Maxime Dénès2020-02-251-0/+4
* Made SmtCommands independent from VeritSyntaxChantal Keller2019-09-254-4/+11
* 3rdpartyChantal Keller2019-07-154-35/+41
* Separate unit tests into vernac and tacticsChantal Keller2019-04-123-12/+7
* Properly check veriT exit code and warnings (#48)ckeller2019-04-124-0/+4
* Error message to state that tactics are not supported with native-coq (#47)ckeller2019-04-126-6/+129
* V8.9 (#43)ckeller2019-03-1510-37/+2708
* Support for native-coqChantal Keller2019-03-122-9/+14
* V8.8 (#42)ckeller2019-03-117-317/+441
* No hard-coded paths to executables (fixes #37)Chantal Keller2019-03-053-887/+2
* V8.7 (#36)ckeller2019-02-1412-647/+1025
* CleanupChantal Keller2019-01-292-7/+1
* Merge from LFSC (#26)ckeller2019-01-2819-109/+407
* Adding support for lemmas in the command veritQuentin Garchery2018-10-286-2/+40
* New files SmtBtype.ml(i) for module formerly in SmtAtomQuentin Garchery2018-10-285-2/+11
* Updated Makefile instructionsQuentin Garchery2018-10-272-12/+17
* formattingQuentin Garchery2018-10-271-1/+1
* conversion tacticsValentin Blot2018-10-254-6/+8
* now compiles with standard coq (including 8.6.1 from opam)Valentin Blot2018-07-206-11/+113
* - 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-032-0/+14
* make install for Coq-8.6Chantal Keller2017-10-032-10/+4
* Tests for Coq-8.6Chantal Keller2017-10-032-6/+31
* Removed unused fileChantal Keller2017-10-031-62/+0
* 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
generated by cgit (git 2.34.1) at 2024-06-26 17:09:18 +0000