aboutsummaryrefslogtreecommitdiffstats
path: root/src/verit
Commit message (Expand)AuthorAgeFilesLines
* Extraction for Coq 8.13 (#109)ckeller2022-07-301-0/+9
* Clean-upChantal Keller2022-04-141-1/+1
* Merge remote-tracking branch 'origin/coq-8.11' into timeout_veritChantal Keller2022-04-146-6/+6
|\
| * Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2022-02-176-6/+6
| |\
| | * Update copyrightChantal Keller2022-02-166-6/+6
* | | use of anomaly for timeoutlduboisd2022-04-081-1/+1
* | | verit timeoutlduboisd2021-12-102-6/+12
|/ /
* | getting rid of native-coq (#95)vblot2021-05-283-16/+16
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-266-6/+6
|\|
| * Update copyrightChantal Keller2021-05-266-6/+6
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-212-2/+12
|\|
| * Convert hypotheses from Prop to bool (#89)ckeller2021-04-212-2/+12
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-02-234-18/+18
|\|
| * Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-234-18/+18
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2020-03-311-3/+10
|\|
| * veriT does not distinguish between warnings and errors (#64)Chantal Keller2020-03-031-0/+2
| * Better error messages when veriT failsChantal Keller2020-02-281-3/+8
* | Compiles with Coq-8.10Chantal Keller2020-03-311-2/+2
|/
* Made SmtCommands independent from VeritSyntaxChantal Keller2019-09-254-104/+53
* Properly check veriT exit code and warnings (#48)ckeller2019-04-121-9/+13
* Check again that veriT returns a zero exit codeChantal Keller2019-04-121-1/+1
* Remove check of veriT non-zero exit codeChantal Keller2019-04-101-1/+1
* V8.8 (#42)ckeller2019-03-111-8/+8
* V8.7 (#36)ckeller2019-02-142-47/+42
* equalities on array and bv types (#34)QGarchery2019-02-121-1/+1
* Fix passing the goal strongly hashed (in ra' rf') instead of normal goal (has...QGarchery2019-02-072-22/+22
* Merge from LFSC (#26)ckeller2019-01-286-275/+532
* verit also works when it doesn't use the conclusion (#24)QGarchery2018-12-031-28/+3
* forall declaration can now begin with a negation (#23)QGarchery2018-11-302-2/+2
* Adding support for lemmas in the command veritQuentin Garchery2018-10-286-114/+378
* New files SmtBtype.ml(i) for module formerly in SmtAtomQuentin Garchery2018-10-284-11/+11
* formattingQuentin Garchery2018-10-273-192/+194
* now compiles with standard coq (including 8.6.1 from opam)Valentin Blot2018-07-201-1/+1
* - auto-generated mli files for future documentationValentin Blot2017-11-241-0/+31
* Allow premices of the transitivity rule to be reflexivity lemmasChantal Keller2016-11-021-8/+15
* Corrected a bug with holes in proofsChantal Keller2016-10-071-2/+2
* Correct parsing of <-> for veriTChantal Keller2016-05-021-0/+2
* Holes in proof:Chantal Keller2016-04-304-4/+8
* Updating of the copyrightChantal Keller2016-04-275-10/+13
* Both native-coq and Coq 8.5 are fully supportedChantal Keller2016-04-262-3/+3
* - Solved the Coq 8.5 problem relating to declaring section variablesChantal Keller2016-04-261-8/+8
* Code refactoringChantal Keller2016-03-021-354/+10
* Separate verit input (smtlib2) from outputChantal Keller2016-03-025-831/+0
* Identify ML functions that are implemented differently in native-coq and in s...Chantal Keller2015-01-131-49/+9
* Identify ML functions that depend on native-coqChantal Keller2015-01-131-6/+6
* Initial import of SMTCoq v1.2Chantal Keller2015-01-1210-0/+2124
generated by cgit (git 2.34.1) at 2024-05-18 20:18:04 +0000