aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Compatibility after Coq PR#262.Gravatar Hugo Herbelin2018-05-14
* finish pushing through changes to dummy and factor out identifier matchGravatar Jade Philipoom2018-05-07
* replace dummy_var with dummy_arrow and change style of straightline tests to ...Gravatar Jade Philipoom2018-05-07
* clean up shared notations and constant-rewriting logic for prefancyGravatar Jade Philipoom2018-05-07
* prefancy now works on barrett (modulo add-opp=>sub)Gravatar Jade Philipoom2018-05-07
* Move straightline and prefancy stuff above barrett reductionGravatar Jade Philipoom2018-05-07
* Translating to 'pre-fancy' form now works on MontgomeryGravatar Jade Philipoom2018-05-07
* move depth to a more sensible locationGravatar Jade Philipoom2018-05-07
* Translation to straightline code now works correctly on montgomery256Gravatar Jade Philipoom2018-05-07
* Translation to straightline code (first attempts, mostly working)Gravatar Jade Philipoom2018-05-07
* fix the placement of a dlet to make more senseGravatar Jade Philipoom2018-05-07
* Backtrack on moving a notation to Notations.v, to fix conflictGravatar Jason Gross2018-05-06
* Fix notations to not conflict with bbvGravatar Jason Gross2018-05-06
* More reserved notationsGravatar Jason Gross2018-05-06
* Add another notationGravatar Jason Gross2018-05-06
* Fix a typo in last commitGravatar Jason Gross2018-05-06
* Add a reserved notation for #vGravatar Jason Gross2018-05-06
* Don't use vm_compute with existentialsGravatar Jason Gross2018-05-05
* Update commentGravatar Jason Gross2018-05-05
* Fully finish flat_mapGravatar Jason Gross2018-05-05
* Fix flat_mapGravatar Jason Gross2018-05-05
* WIP on lists as cons cellsGravatar Jason Gross2018-05-05
* Remove vinterp_arrow functionGravatar Jason Gross2018-05-05
* Revert "WIP on inductive base_value"Gravatar Jason Gross2018-05-05
* WIP on inductive base_valueGravatar Jason Gross2018-05-05
* Revert "WIP with andres, not working pattern language"Gravatar Jason Gross2018-05-05
* WIP with andres, not working pattern languageGravatar Jason Gross2018-05-05
* Add comment about leaky abstractionGravatar Jason Gross2018-05-05
* Split off specialization to base types from specialization to identsGravatar Jason Gross2018-05-05
* Add type variables / substitutionsGravatar Jason Gross2018-05-05
* Change some notations for more readability by AndresGravatar Jason Gross2018-05-05
* Update cast -> annotateGravatar Jason Gross2018-05-05
* Parameterize over types and identifiersGravatar Jason Gross2018-05-05
* Add notesGravatar Jason Gross2018-05-05
* Add partial evaluationGravatar Jason Gross2018-05-05
* Some experiments with partial evaluation with letin without cpsGravatar Jason Gross2018-05-05
* un-hardcode # of reductionsGravatar Jade Philipoom2018-04-30
* print saturated mulmod for p192 on 32-bit, add note about p256Gravatar Jade Philipoom2018-04-30
* fixed too-many-additions problem by fixing number of limbs in from_associationalGravatar Jade Philipoom2018-04-30
* Fix some carry logicGravatar Jade Philipoom2018-04-30
* First stab at generating code for saturated solinas modularGravatar Jade Philipoom2018-04-30
* fix commentGravatar Jade Philipoom2018-04-30
* Fix bounds analysis for saturated ops and remove unneeded commentGravatar Jade Philipoom2018-04-30
* first stab at reifying barrettGravatar Jade Philipoom2018-04-30
* fix definitions of saturated operations to avoid unnecessary work, and make M...Gravatar Jade Philipoom2018-04-30
* tweak definition of flatten to use an index rather than check the length of t...Gravatar Jade Philipoom2018-04-30
* fix the placement of a dlet to make more senseGravatar Jade Philipoom2018-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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 10:29:57 +0000