aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* Make use of expand_lists tacticGravatar Jason Gross2018-02-18
* Rename carry_mulmod_correct to eval_carry_mulmod to fit with other lemmasGravatar Jason Gross2018-02-18
* Add GallinaReify.AutoReifyGravatar Jason Gross2018-02-18
* Simplify the pipeline a bitGravatar Jason Gross2018-02-18
* Remove try_transport_untranslateGravatar Jason Gross2018-02-18
* Respond to some code review commentsGravatar Jason Gross2018-02-18
* Do a large chunk of the bounds pipelineGravatar Jason Gross2018-02-18
* WIP on more general continuationsGravatar Jason Gross2018-02-18
* Add notations for type reificationGravatar Jason Gross2018-02-18
* Add some imports to experimentsGravatar Jason Gross2018-02-18
* Strip the pointed instance names off of the default value in list expansionGravatar Jason Gross2018-02-18
* Add expand_lists tacticGravatar Jason Gross2018-02-18
* Add pointed typesGravatar Jason Gross2018-02-18
* Fix a proof for Coq 8.7Gravatar Jason Gross2018-02-17
* Add lemmas about always_invert_Some and bindGravatar Jason Gross2018-02-17
* Add always_invert_SomeGravatar Jason Gross2018-02-17
* Add commentGravatar Jason Gross2018-02-16
* Fix CPSify of bool_rect to eliminate dead codeGravatar Jason Gross2018-02-16
* Move [Section invert] above CPSGravatar Jason Gross2018-02-16
* Add a file to parse taps with Coq notationsGravatar Jason Gross2018-02-14
* Add some string utility functionsGravatar Jason Gross2018-02-13
* Add expand_list_correct to ListUtilGravatar Jason Gross2018-02-12
* Add some TODOsGravatar Jason Gross2018-02-12
* [experiments] Use smaller multiplication for 19*x (#307)Gravatar Jason Gross2018-02-12
* Add string conversionsGravatar Jason Gross2018-02-11
* [Work in Progress] Experiment with Bounds Analysis based on lists (#305)Gravatar Jason Gross2018-02-11
* Add notation for option_bindGravatar Jason Gross2018-02-10
* Split off ZRange lemmasGravatar Jason Gross2018-02-10
* Add some ZRange operationsGravatar Jason Gross2018-02-10
* minor updates needed to make it compile with bbvGravatar Samuel Gruetter2018-02-05
* Add dead code elimination via inliningGravatar Jason Gross2018-01-29
* Have reification run delta on unknown identsGravatar Jason Gross2018-01-29
* Remove useless dletGravatar Jason Gross2018-01-29
* Change reduction behavior of let-bound listsGravatar Jason Gross2018-01-29
* Use Derive plugin, do two passes of partial reductionGravatar Jason Gross2018-01-29
* rerunGravatar Andres Erbsen2018-01-29
* fix carry chain in exampleGravatar Andres Erbsen2018-01-29
* Respond to some CR commentsGravatar Jason Gross2018-01-29
* Don't reify [let ... in ...], only [dlet ... in ...]Gravatar Jason Gross2018-01-29
* Write ltamer-based CPS transformGravatar Jason Gross2018-01-29
* Fix weight to use 51-bit limbsGravatar Jason Gross2018-01-29
* Remove use of beta in reification of Let_InGravatar Jason Gross2018-01-29
* Rename type.opaque to type.primitiveGravatar Jason Gross2018-01-29
* remove outdated commentGravatar Jason Gross2018-01-29
* Get cps for carry workingGravatar Jason Gross2018-01-29
* Support Let_in with not-fully-reduced second arg in reificationGravatar Jason Gross2018-01-29
* More types in type_opaque; restore nth_default notationGravatar Jason Gross2018-01-29
* Remove dead codeGravatar Jason Gross2018-01-29
* Add a CPS conversion passGravatar Jason Gross2018-01-29
* make SimplyTypedArithmetic less "Smart" by giving every expression a normal formGravatar Andres Erbsen2018-01-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 08:18:09 +0000