aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Make IsIso a classGravatar Jason Gross2016-07-29
* Add HProp, IsomorphismGravatar Jason Gross2016-07-29
* Add inversion helper tactics to Sigma.vGravatar Jason Gross2016-07-29
* Rename path_sig{,T}{ => _uncurried}_iffGravatar Jason Gross2016-07-29
* Add path_sig{,T}_iffGravatar Jason Gross2016-07-29
* Add some lemmas to Util.SigmaGravatar Jason Gross2016-07-29
* Set Asymmetric Patterns, add util lemmas about sigGravatar Jason Gross2016-07-29
* Get rid of unparsable unicode notationGravatar Jason Gross2016-07-28
* Add more reserved notationsGravatar Jason Gross2016-07-28
* Add instances about congruence moduloGravatar Jason Gross2016-07-28
* Add unicode reserved notationsGravatar Jason Gross2016-07-28
* Add Z.mod_mod to zsimplifyGravatar Jason Gross2016-07-28
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
* Restore functionality of Z.simplify_fractions_leGravatar Jason Gross2016-07-27
* Make Z.pre_reorder_fractions / Z.simplify_fractions_le not loopGravatar Jason Gross2016-07-27
* Add another ZUtil lemmaGravatar Jason Gross2016-07-26
* Fix 8.4 build.Gravatar jadep2016-07-25
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-25
|\
* | A couple new util lemmasGravatar jadep2016-07-25
| * More Zpow in ZUtilGravatar Jason Gross2016-07-22
| * More ZUtilGravatar Jason Gross2016-07-22
| * Add reverse_nondep and ring_simplify_subterms_in_all tacticsGravatar Jason Gross2016-07-22
| * More ZUtil lemmasGravatar Jason Gross2016-07-22
| * Revert "Revert "Add more ZUtil automation""Gravatar Jason Gross2016-07-22
| * Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
| * Revert "Add more ZUtil automation"Gravatar Jason Gross2016-07-22
| * Add more ZUtil automationGravatar Jason Gross2016-07-22
| * Add ring_simplify_subtermsGravatar Jason Gross2016-07-22
| * Generalize div_sub_small a bitGravatar Jason Gross2016-07-22
|/
* Add another lemma to zarithGravatar Jason Gross2016-07-21
* Add another ZUtil lemmaGravatar Jason Gross2016-07-21
* Another ZUtil lemmaGravatar Jason Gross2016-07-21
* Fix broken proofsGravatar Jason Gross2016-07-21
* Add more ZUtilGravatar Jason Gross2016-07-21
* More ZUtil helper lemmasGravatar Jason Gross2016-07-21
* Add more ZUtil lemmasGravatar Jason Gross2016-07-21
* Add ZUtil lemmasGravatar Jason Gross2016-07-21
* Add Z.lt_le_incl to zarithGravatar Jason Gross2016-07-20
* Add another lemma about +, <= to arithGravatar Jason Gross2016-07-20
* Add a distr_length databaseGravatar Jason Gross2016-07-19
* Remove stuff from PseudoMersenneBaseParamProofs.vGravatar Jason Gross2016-07-19
* Add a lemma about sum_firstnGravatar Jason Gross2016-07-18
* Add a ListUtil lemmaGravatar Jason Gross2016-07-18
* Fix for Coq 8.4 (missing lemmas)Gravatar Jason Gross2016-07-18
* Fix for Coq 8.4 (omega used to be weaker)Gravatar Jason Gross2016-07-18
* Add more natsimplify le_dec lemmasGravatar Jason Gross2016-07-18
* Add more NatUtil lemmasGravatar Jason Gross2016-07-18
* Add natsimplify lemmas about eq_nat_decGravatar Jason Gross2016-07-18
* Fix some typos in the previous commitGravatar Jason Gross2016-07-18
* Add some lemmas about nth_default in boundsGravatar Jason Gross2016-07-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 21:54:34 +0000