aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic.v
Commit message (Expand)AuthorAge
* split up Arithmetic (imports etc. not yet fixed, does not build)Gravatar jadep2019-04-03
* improve zero_bounds tacticGravatar jadep2019-03-26
* add some hints to the global databasesGravatar jadep2019-03-26
* remove Derive to fix 8.7Gravatar jadep2019-03-25
* remove 2: syntax so I don't break 8.7Gravatar jadep2019-03-25
* fix up a messy proofGravatar jadep2019-03-25
* Move some lemmas to appropriate placesGravatar jadep2019-03-25
* finish proofsGravatar jadep2019-03-25
* Get new Barrett proofs to generate Fancy code as beforeGravatar jadep2019-03-25
* WIPGravatar jadep2019-03-25
* Add Option.{lift,map,combine}, List.Option.liftGravatar Jason Gross2019-02-11
* Reduce more in mulmod and squaremodGravatar Jason Gross2019-01-26
* Split up PushButtonSynthesis.vGravatar Jason Gross2019-01-18
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09