aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions
Commit message (Expand)AuthorAgeFilesLines
* getting rid of native-coq (#95)vblot2021-05-2821-6119/+0
* Get rid of most of our copy of micromega's source code (#94)vblot2021-05-284-11/+1
* Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-2616-16/+16
|\
| * Update copyrightChantal Keller2021-05-2616-16/+16
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-281-1/+1
|\|
| * prop2bool_hyps insensitive to parenthesisChantal Keller2021-04-281-1/+1
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-261-14/+17
|\|
| * CompDec are automatically discharged when generated by the OCaml tactic, when...Chantal Keller2021-04-261-14/+17
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-261-12/+115
|\|
| * Take hypotheses from the local context (#91)ckeller2021-04-261-12/+115
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-213-30/+15
|\|
| * Convert hypotheses from Prop to bool (#89)ckeller2021-04-213-30/+15
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-02-231-6/+6
|\|
| * Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-231-6/+6
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2020-06-291-1/+5
|\|
| * Remove invalid axiom (see #71)Chantal Keller2020-06-291-1/+5
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2020-03-312-9/+36
|\|
| * 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
* | Compiles with Coq-8.10Chantal Keller2020-03-312-0/+2
* | Port to coq-8.10 under progressChantal Keller2020-03-317-2670/+22
* | Hints in databasesChantal Keller2020-01-282-0/+3
* | Towards coqppChantal Keller2020-01-161-35/+35
* | ml4 -> mlgChantal Keller2020-01-162-1/+1
|/
* 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
generated by cgit (git 2.34.1) at 2024-06-26 14:33:52 +0000