aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtCommands.ml
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2022-02-171-1/+1
|\
| * Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2022-02-171-1/+1
| |\
| | * Update copyrightChantal Keller2022-02-161-1/+1
* | | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12Chantal Keller2022-02-151-69/+61
|\| |
| * | Use the Register mechanism (#104)ckeller2022-02-151-69/+61
* | | Merge branch 'coq-8.11' of github.com:smtcoq/smtcoq into coq-8.12Chantal Keller2021-05-281-216/+216
|\| |
| * | getting rid of native-coq (#95)vblot2021-05-281-216/+216
* | | Merge branch 'coq-8.11' of github.com:smtcoq/smtcoq into coq-8.12Chantal Keller2021-05-261-1/+1
|\| |
| * | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-261-1/+1
| |\|
| | * Update copyrightChantal Keller2021-05-261-1/+1
* | | Port ocaml partChantal Keller2021-05-261-1/+1
|/ /
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-281-2/+6
|\|
| * Solve a bug when reifying under a binderChantal Keller2021-04-281-2/+6
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-211-15/+15
|\|
| * Solve a bound variable capture problem in the reification of quantified hypot...Chantal Keller2021-04-211-15/+15
* | Port to 8.10Chantal Keller2021-04-211-1/+1
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-04-211-16/+41
|\|
| * Warning (instead of error) for unsupported lemmas (#90)ckeller2021-04-211-16/+41
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-02-231-21/+21
|\|
| * Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-231-21/+21
* | Compiles with Coq-8.10Chantal Keller2020-03-311-1/+1
|/
* Made SmtCommands independent from VeritSyntaxChantal Keller2019-09-251-2/+2
* V8.8 (#42)ckeller2019-03-111-176/+164
* V8.7 (#36)ckeller2019-02-141-118/+118
* Fix passing the goal strongly hashed (in ra' rf') instead of normal goal (has...QGarchery2019-02-071-13/+14
* Merge from LFSC (#26)ckeller2019-01-281-99/+609
* Adding support for lemmas in the command veritQuentin Garchery2018-10-281-22/+89
* New files SmtBtype.ml(i) for module formerly in SmtAtomQuentin Garchery2018-10-281-1/+1
* formattingQuentin Garchery2018-10-271-7/+5
* Corrected a bug with holes in proofsChantal Keller2016-10-071-10/+9
* Hopefully solved the problem with universes for the tacticChantal Keller2016-09-281-10/+35
* Improved performance with coq-8.5Chantal Keller2016-09-281-13/+28
* Print warnings when checking proofs with holesChantal Keller2016-04-301-5/+27
* Bring back the nice printing of automatically generated theoremsChantal Keller2016-04-301-8/+8
* Solved the efficiency problemChantal Keller2016-04-301-34/+83
* Holes in proof:Chantal Keller2016-04-301-6/+22
* Possibility to embed any Coq proof in certificates (not tested yet)Chantal Keller2016-04-291-67/+70
* Updating of the copyrightChantal Keller2016-04-271-0/+16
* Both native-coq and Coq 8.5 are fully supportedChantal Keller2016-04-261-6/+5
* Compatibility with native-coqChantal Keller2016-04-261-5/+5
* Tactic verit for 8.5Chantal Keller2016-04-261-4/+4
* Light port to Coq 8.5 under progressChantal Keller2016-03-181-4/+4
* Code refactoringChantal Keller2016-03-021-0/+256
generated by cgit (git 2.34.1) at 2024-06-26 16:55:49 +0000