aboutsummaryrefslogtreecommitdiff
path: root/src/Util/CPSUtil.v
Commit message (Expand)AuthorAge
* Deduplicate some codeGravatar Jason Gross2017-11-06
* More id_with_alt_cps updatesGravatar Jason Gross2017-11-06
* Update versions of id_with_alt_cpsGravatar Jason Gross2017-11-06
* Add cps versions of id_with_altGravatar Jason Gross2017-11-01
* Factor out fold_right_cps2_specialized_step, add mapi_with'_cps2Gravatar Jason Gross2017-10-22
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-18
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-17
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-17
* Allow instantiation of cps type arguments by unfoldingGravatar Jason Gross2017-10-17
* Allow unfolding of mapi_with_cps to specialize the function to the type argum...Gravatar Jason Gross2017-10-17
* remove unused admit (has been moved to Tuple.v)Gravatar jadep2017-06-26
* Prove map2_appendGravatar Jason Gross2017-06-25
* write and prove Tuple.map2_cpsGravatar jadep2017-06-25
* Prove In_to_list_left_tl, In_left_hd, to_list_left_appendGravatar Jason Gross2017-06-21
* finish tuple-ifying Montgomery APIGravatar jadep2017-06-16
* CPSify Saturated API in preparation for CPSifying Montgomery (see #194)Gravatar jadep2017-06-15
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
* add Tuple.map_cps to CPSUtilGravatar jadep2017-05-01
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* remove commented-out lemma and add CPS version of mapi_withGravatar jadep2017-03-29
* Merge new base system (#112)Gravatar jadephilipoom2017-02-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-30 23:49:55 +0000