aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
| | * Slightly better arguments in ListUtilGravatar Jason Gross2016-07-07
| | * Correct hintdb namesGravatar Jason Gross2016-07-07
| | * Add more about firstn to listutilGravatar Jason Gross2016-07-07
| | * Add more update_nth to ListUtilGravatar Jason Gross2016-07-07
| | * Fix ListUtil for Coq 8.4Gravatar Jason Gross2016-07-07
| | * Add pow2_mod to ZUtilGravatar Jason Gross2016-07-07
| |/
| * Changed [auto]s to [eauto]s in ModularBaseSystemProofs for 8.5 compatibility.Gravatar jadep2016-07-07
| * Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-07
| |\
| | * Fix notations, add &Gravatar Jason Gross2016-07-06
| | * Add [update_nth] to ListUtil, change [set_nth]Gravatar Jason Gross2016-07-06
| | * Add notations for Z.shift{r,l} to ZUtilGravatar Jason Gross2016-07-06
| | * Improve some reserved notationsGravatar Jason Gross2016-07-06
| | * Add a TODO commentGravatar Jason Gross2016-07-06
| * | Proved lingering lemmas in PointEncodingPre.Gravatar jadep2016-07-06
| | * Fix for broken 8.5 build in ListUtilGravatar Jason Gross2016-07-06
| |/
| * fixed indentation for new lemmas in ZUtilGravatar jadep2016-07-06
| * Merged changes, including new ZUtil conventions.Gravatar jadep2016-07-06
| |\
| * \ Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-07-06
| |\ \
| * | | Factored out some proofs that rely only on base being powers of two, and defi...Gravatar jadep2016-07-06
* | | | stuck trying to figure out dependently typed continuation passing styleGravatar Andres Erbsen2016-07-06
* | | | add new interface to ModularBaseSystemGravatar Andres Erbsen2016-07-03
* | | | Tuple: lift functions from lists to tuplesGravatar Andres Erbsen2016-07-03
* | | | remove PseudoMersenneRepGravatar Andres Erbsen2016-07-03
| | | * Define the spec of Weierstrass curves (#6)Gravatar Jason Gross2016-07-03
| | | * Implement and prove Barrett reduction on Z (#18)Gravatar Jason Gross2016-07-03
| | | * Indentation in ZUtilGravatar Jason Gross2016-07-02
| | | * Make ZUtil more uniformGravatar Jason Gross2016-07-02
| | | * super_nsatz: Handle x^2 = y^2 -> x <> -y -> x = yGravatar Jason Gross2016-07-02
| |_|/ |/| |
* | | Fix for 8.4 evarsGravatar Jason Gross2016-07-01
* | | Add ZUtil hintsGravatar Jason Gross2016-07-01
* | | Add more hints to ZUtilGravatar Jason Gross2016-07-01
* | | Add more hints in ZUtilGravatar Jason Gross2016-07-01
* | | Add more ZUtil hintsGravatar Jason Gross2016-07-01
* | | Add more hints to ZUtilGravatar Jason Gross2016-07-01
* | | Simplify a proof that no longer needs more hintsGravatar Jason Gross2016-07-01
* | | Add hint databases and a proof about Z.log2Gravatar Jason Gross2016-07-01
* | | Add some proofs about Z.div and Z.mulGravatar Jason Gross2016-07-01
* | | Add [specialize_by] tacticGravatar Jason Gross2016-07-01
* | | Fix a typo in Zsplit_sumsGravatar Jason Gross2016-07-01
* | | Add tactic to split sums and differences in inequalitiesGravatar Jason Gross2016-07-01
* | | Add fraction inequality reasoning tactics to ZUtilGravatar Jason Gross2016-07-01
* | | Add a proof of 2 * x - x = xGravatar Jason Gross2016-06-30
* | | Add a classification of n / m < 0Gravatar Jason Gross2016-06-30
* | | Add a tactic for making use of destructed <? in ZGravatar Jason Gross2016-06-30
* | | Prove that a ^ k <> 0Gravatar Jason Gross2016-06-30
| * | added and proved shift/or decode operation 'decode_bitwise'Gravatar jadep2016-06-30
* | | Add pow_Zpow to Util.ZUtilGravatar Jason Gross2016-06-30
* | | Simplify conservative_common_denominatorGravatar Jason Gross2016-06-29
* | | Don't generate goals [False] in conservative_common_denominator_allGravatar Jason Gross2016-06-29
* | | Fix [only_two_square_roots] to not loopGravatar Jason Gross2016-06-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-30 02:12:26 +0000