aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Fix zrange notation levelsGravatar Jason Gross2017-06-12
* Add CompileInterpSideConditions.vGravatar Jason Gross2017-06-12
* Add snd_interpf_side_conditions_gen_SomeGravatar Jason Gross2017-06-12
* Add Named.InterpSideConditionsGravatar Jason Gross2017-06-12
* Handle multiple lite-unmade-vofilesGravatar Jason Gross2017-06-12
* Fix lite target (typo in makefile fn call)Gravatar Jason Gross2017-06-12
* Add Z.InterpSideConditionsGravatar Jason Gross2017-06-12
* Add InterpSideConditionsGravatar Jason Gross2017-06-12
* Have interped_op_side_conditions return a pointed_PropGravatar Jason Gross2017-06-12
* Better support for coq_makefile2 with fewer warningsGravatar Jason Gross2017-06-12
* Drop unused [bn] notationGravatar Jason Gross2017-06-12
* Drop some small hyps in light of small_add changeGravatar Jason Gross2017-06-12
* Remove eval_small_bounded_numlimbsGravatar Jason Gross2017-06-12
* Initial stab at id_with_altGravatar Jason Gross2017-06-11
* Add dummy version of IdWithAlt to compilersGravatar Jason Gross2017-06-11
* Factor karatsuba through IdfunWithAlt, add testGravatar Jason Gross2017-06-11
* Add unfold lemmas for id_with_altGravatar Jason Gross2017-06-11
* Add IdfunWithAltGravatar Jason Gross2017-06-11
* Don't print directory when entering coqprime folderGravatar Jason Gross2017-06-11
* Be more forceful about clearing before abstract in glue codeGravatar 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
* Finish admits in WordByWord/Proofs.vGravatar Jason Gross2017-06-10
* 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
* Minor changes to a proof in progressGravatar Jason Gross2017-06-10
* Remove useless small_from_bound; drop R_bigGravatar Jason Gross2017-06-10
* Add proofs about numlimbsGravatar Jason Gross2017-06-10
* Add constraint on scmul scalarGravatar Jason Gross2017-06-10
* Update context to not need eval_nonnegGravatar Jason Gross2017-06-10
* Add redc_boundGravatar Jason Gross2017-06-10
* Create crypto-defects.mdGravatar Andres Erbsen2017-06-10
* Remove temporary fileGravatar Jason Gross2017-06-10
* More work in progress on montgomery proofsGravatar Jason Gross2017-06-10
* More work on redc correctness proofsGravatar Jason Gross2017-06-10
* Add initial proofs for word-by-wordGravatar Jason Gross2017-06-10
* Switch from t to T to match #157Gravatar Jason Gross2017-06-10
* Update redc algorithmGravatar Jason Gross2017-06-10
* Update word-by-word montgomery with ctx varsGravatar Jason Gross2017-06-10
* Finish proving loop invariant for wbw redcGravatar Jason Gross2017-06-09
* Make it clear that the combined definition/proof file is a work in progressGravatar Jason Gross2017-06-09
* Admit-free proof of cS3_mod_NGravatar Jason Gross2017-06-09
* Fix open sections errorGravatar Jason Gross2017-06-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-02 00:42:04 +0000