aboutsummaryrefslogtreecommitdiff
path: root/src/Util/CPSUtil.v
Commit message (Expand)AuthorAge
* 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