aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtCommands.ml
Commit message (Expand)AuthorAgeFilesLines
* Update copyrightChantal Keller2022-02-161-1/+1
* Update copyrightChantal Keller2021-05-261-1/+1
* Solve a bug when reifying under a binderChantal Keller2021-04-281-2/+6
* Solve a bound variable capture problem in the reification of quantified hypot...Chantal Keller2021-04-211-15/+15
* Warning (instead of error) for unsupported lemmas (#90)ckeller2021-04-211-16/+41
* Link equality on uninterpreted sorts with SMT equality (#86)ckeller2021-02-231-21/+21
* 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-29 08:30:17 +0000