aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* finish tuple-ifying Montgomery APIGravatar jadep2017-06-16
* CPSify Saturated API in preparation for CPSifying Montgomery (see #194)Gravatar jadep2017-06-15
* Don't force [Require Import String] for debug msgsGravatar Jason Gross2017-06-15
* Fix a changed case in the proof in loop.vGravatar Jason Gross2017-06-15
* Better for_loop induction principleGravatar Jason Gross2017-06-15
* Export ZUtil.Z2Nat in ZUtilGravatar Jason Gross2017-06-15
* Add ZUtil.Z2NatGravatar Jason Gross2017-06-15
* Add for_cps_unroll1Gravatar Jason Gross2017-06-15
* Add eq_loop_cps_large_nGravatar Jason Gross2017-06-15
* move CPS notations to Util.CPSNotationsGravatar Andres Erbsen2017-06-15
* Loop changes, ScalarMultBase_correct with admitsGravatar Andres Erbsen2017-06-14
* loops WIPGravatar Andres Erbsen2017-06-14
* ScalarMult: Z -> G -> G (closes #193)Gravatar Andres Erbsen2017-06-14
* Add mul_split_at_bitwidth, define things in terms of thatGravatar Jason Gross2017-06-13
* Add Z.peano_rect_strongGravatar Jason Gross2017-06-13
* Add dec_eq_comparisonGravatar Jason Gross2017-06-13
* Add Z.peano_rectGravatar Jason Gross2017-06-13
* Add Z.mul_splitGravatar Jason Gross2017-06-13
* Fix zrange notation levelsGravatar Jason Gross2017-06-12
* Add unfold lemmas for id_with_altGravatar Jason Gross2017-06-11
* Add IdfunWithAltGravatar Jason Gross2017-06-11
* Add script to remake Tactics.v fileGravatar Jason Gross2017-06-11
* Add clearbody_allGravatar Jason Gross2017-06-11
* Fix loop notations, add for loopsGravatar Jason Gross2017-06-11
* Reserve some more notationsGravatar Jason Gross2017-06-11
* cps notations WIP...Gravatar Andres Erbsen2017-06-11
* cps and loop notations WIPGravatar Andres Erbsen2017-06-11
* Add mod_pull_div{,_full}Gravatar Jason Gross2017-06-10
* More powerful replace_neg_with_posGravatar Jason Gross2017-06-10
* Fix a typoGravatar Jason Gross2017-06-10
* Rename power_mod_full to mod_pow_full for similarity with std libGravatar Jason Gross2017-06-10
* Add Z.pow_mod_ProperGravatar Jason Gross2017-06-10
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Allow loop notation to printGravatar Jason Gross2017-06-05
* Add an only-parsing loop notationGravatar Jason Gross2017-06-02
* Add experimental loopsGravatar Jason Gross2017-06-02
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
* Add adc -> sbb to arithmetic simpliferGravatar Jason Gross2017-05-20
* Add SubWithGetBorrow to reflective machineryGravatar Jason Gross2017-05-20
* Add subst_prod tactic to Prod.vGravatar Jason Gross2017-05-19
* Update adc lemmas to version freeze actually usesGravatar Jason Gross2017-05-17
* Revert "Add dec_eq_positive"Gravatar Jason Gross2017-05-16
* Add dec_eq_positiveGravatar Jason Gross2017-05-16
* Add more pointed prop lemmasGravatar Jason Gross2017-05-15
* More debug info in reificationGravatar Jason Gross2017-05-14
* add wrapper for add_get_carry and proofs for add_get_carry and zselectGravatar jadep2017-05-14
* Add lemma justifying compiler optimization for adcGravatar Jason Gross2017-05-14
* Fix notation binding levels so types work in nletGravatar Jason Gross2017-05-14
* Add some reserved notationsGravatar Jason Gross2017-05-14
* Allow specifying type in nletGravatar Jason Gross2017-05-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 09:33:28 +0000