aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/standard
Commit message (Expand)AuthorAgeFilesLines
* getting rid of native-coq (#95)vblot2021-05-2814-4927/+0
* Get rid of most of our copy of micromega's source code (#94)vblot2021-05-282-7/+1
* Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-2611-11/+11
|\
| * Update copyrightChantal Keller2021-05-2611-11/+11
* | 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-252-0/+3
* 3rdpartyChantal Keller2019-07-152-9/+11
* Separate unit tests into vernac and tacticsChantal Keller2019-04-121-1/+1
* 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-122-0/+66
* V8.9 (#43)ckeller2019-03-158-32/+2703
* V8.8 (#42)ckeller2019-03-115-208/+264
* No hard-coded paths to executables (fixes #37)Chantal Keller2019-03-053-887/+2
* V8.7 (#36)ckeller2019-02-1410-644/+997
* CleanupChantal Keller2019-01-292-7/+1
* Merge from LFSC (#26)ckeller2019-01-2813-82/+227
* Adding support for lemmas in the command veritQuentin Garchery2018-10-283-1/+22
* New files SmtBtype.ml(i) for module formerly in SmtAtomQuentin Garchery2018-10-283-0/+5
* Updated Makefile instructionsQuentin Garchery2018-10-271-6/+8
* conversion tacticsValentin Blot2018-10-252-6/+6
* now compiles with standard coq (including 8.6.1 from opam)Valentin Blot2018-07-204-11/+108
* Compiles with both versions of CoqChantal Keller2017-10-031-0/+7
* 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 proofsChantal Keller2016-10-071-2/+2
generated by cgit (git 2.34.1) at 2024-06-26 15:38:29 +0000