aboutsummaryrefslogtreecommitdiff
path: root/src/BoundedArithmetic/ArchitectureToZLikeProofs.v
Commit message (Expand)AuthorAge
* rename-everythingGravatar Andres Erbsen2017-04-06
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Split up DoubleBoundedProofs, add proofsGravatar Jason Gross2016-10-07
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-10-03
* Drop CSE from Fancy MachineGravatar Jason Gross2016-09-22
* Use dlet, not lletGravatar Jason Gross2016-09-22
* Don't inline everything in Montgomery and BarrettGravatar Jason Gross2016-09-22
* Integrate suggestions from AndresGravatar Jason Gross2016-08-25
* Rework bounded proofsGravatar Jason Gross2016-08-24
* Weaken the condition on smaller_boundGravatar Jason Gross2016-08-23
* Hook up the bounded interface, finish proofsGravatar Jason Gross2016-08-23