aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Minor refactoringGravatar Jason Gross2018-06-13
* Add PrimitiveHList, PrimitiveProdGravatar Jason Gross2018-06-13
* Move Option.List.map to OptionList.map to fix name clashes in TupleGravatar Jason Gross2018-06-04
* Add Option.List.mapGravatar Jason Gross2018-06-04
* Move cps notations into a scopeGravatar Jason Gross2018-06-01
* Add more bind reserved notationsGravatar Jason Gross2018-05-31
* fix over-indented lineGravatar Jade Philipoom2018-05-31
* prove prefancy->fancy for barrett special caseGravatar Jade Philipoom2018-05-31
* move around some Lets so that 8.8 doesn't errorGravatar Jade Philipoom2018-05-31
* relocate ok_expr tactics and fix an admit with a silly bounds relaxation hackGravatar Jade Philipoom2018-05-31
* Proved pre-fancy barrett reduction correct (except 1 admit for boundsGravatar Jade Philipoom2018-05-31
* temporary workaround for #352Gravatar Jade Philipoom2018-05-31
* Define machine model, write prefancy->fancy pass, and prove Montgomery code c...Gravatar Jade Philipoom2018-05-31
* [WIP] shifting addsGravatar Jade Philipoom2018-05-31
* change order of additions so that they a) make more sense and b) are more sui...Gravatar Jade Philipoom2018-05-31
* tweak binders so that shifts from base conversion get inlinedGravatar Jade Philipoom2018-05-31
* remove unneeded comment and extra whitespaceGravatar Jade Philipoom2018-05-31
* end-to-end proof for montgomeryGravatar Jade Philipoom2018-05-31
* Proofs for pre-fancy pass (could use cleanup)Gravatar Jade Philipoom2018-05-31
* proofs for straightline pass (with admits for some depth stuff that should be...Gravatar Jade Philipoom2018-05-31
* Move function argument out of fixpoint of List.map2Gravatar Jason Gross2018-05-21
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 13:05:03 +0000