aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Don't allow coqprime and coqprime-all to run in parallelGravatar Jason Gross2018-04-30
* Only install files built by the coq targetGravatar Jason Gross2018-04-30
* Add a coqprime-all target to build all of coqprimeGravatar Jason Gross2018-04-30
* In reassocation, don't reassociate additionsGravatar Jason Gross2018-04-26
* Fix a printoutGravatar Jason Gross2018-04-26
* Revert most of "Make reassociation optional"Gravatar Jason Gross2018-04-26
* Make reassociation optionalGravatar Jason Gross2018-04-26
* Compute tight bounds in a different wayGravatar Jason Gross2018-04-26
* Don't introduce extra lambdas and apps in uncurryGravatar Jason Gross2018-04-26
* Add some Positional Hint RewritesGravatar Jason Gross2018-04-26
* Util.Loops: remove non-stdlib dependenciesGravatar Andres Erbsen2018-04-26
* Generalize Jacobian.v over all a.Gravatar David Benjamin2018-04-25
* Fix the lite-display targetGravatar Jason Gross2018-04-20
* pass-through after Jason's reviewGravatar Jade Philipoom2018-04-19
* add instructions cc_m, rshi, and sub_with_get_borrow to pipeline in preparati...Gravatar Jade Philipoom2018-04-19
* Also include argument bounds in bounds-analysis-failure messageGravatar Jason Gross2018-04-18
* Add COQLIBS to display targetsGravatar Jason Gross2018-04-18
* Error if a display target failsGravatar Jason Gross2018-04-18
* Fix a proofGravatar Jason Gross2018-04-18
* Change a proof in src/Util/OptionGravatar Jason Gross2018-04-18
* Merge pull request #335 from mit-plv/cpsloopsGravatar Andres Erbsen2018-04-18
|\
* | Actually display the error messages from pipeline failuresGravatar Jason Gross2018-04-18
* | Add a Z.cast2 case to bounds extractionGravatar Jason Gross2018-04-18
* | Also include the syntax tree in bounds analysis errorsGravatar Jason Gross2018-04-18
* | Bump coq-scripts to fix a bugGravatar Jason Gross2018-04-15
* | Add a lite-display targetGravatar Jason Gross2018-04-15
* | Bump coq-scriptsGravatar Jason Gross2018-04-15
* | move requires to top of fileGravatar Jade Philipoom2018-04-11
* | barrett reduction definition and proofGravatar Jade Philipoom2018-04-11
* | add a list lemmaGravatar Jade Philipoom2018-04-11
* | add some lemmas aboud div and modGravatar Jade Philipoom2018-04-11
* | Add new assembly-mimicking operations rshi, cc_m, and cc_lGravatar Jade Philipoom2018-04-11
* | fix trashed carry flagGravatar Jade Philipoom2018-04-11
* | remove commentGravatar Jade Philipoom2018-04-11
* | add a comment to rerun buildGravatar Jade Philipoom2018-04-11
* | Automate some proofs a bit moreGravatar Jason Gross2018-04-11
* | try to fix build on coq masterGravatar Jade Philipoom2018-04-11
* | prove stronger bound on quotient error for barrett reductionGravatar Jade Philipoom2018-04-11
* | Update number/string conversionsGravatar Jason Gross2018-04-09
* | package properties of weight functions into a recordGravatar Jade Philipoom2018-04-09
* | relocate and prove an admitGravatar Jade Philipoom2018-04-09
* | update coqprimeGravatar Jade Philipoom2018-04-09
* | reorganization: move more things into BaseConversionGravatar Jade Philipoom2018-04-09
* | better factoring-out of mul_converted stuff, define saturated arith operationsGravatar Jade Philipoom2018-04-06
* | Use a simpler form of UncurryingGravatar Jason Gross2018-04-04
* | Stick an uncurry pass in the pipelineGravatar Jason Gross2018-04-04
* | Add UncurryGravatar Jason Gross2018-04-04
* | Update coqprimeGravatar Jason Gross2018-04-03
* | Update .mailmapGravatar Jason Gross2018-04-03
* | pass-through after Jason's reviewGravatar Jade Philipoom2018-04-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-14 02:30:19 +0000