aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Add tactics to implement better fraction removalGravatar Jason Gross2016-10-26
* prove SRepMul admitGravatar Andres Erbsen2016-10-25
* Fix for Coq 8.4Gravatar Jason Gross2016-10-24
* Add more relations about fieldwiseGravatar Jason Gross2016-10-24
* More 8.4 fixesGravatar Jason Gross2016-10-23
* Fix 8.4 build issueGravatar Jason Gross2016-10-23
* Prove an admitted NatUtil lemmaGravatar Jason Gross2016-10-23
* Prove more things in WordUtilGravatar Jason Gross2016-10-23
* Fill in some word util admitted lemmasGravatar Jason Gross2016-10-23
* Add more specific form of Proper_Let_In_nd_changebodyGravatar Jason Gross2016-10-22
* Add Bool lemmas about if statementsGravatar Jason Gross2016-10-21
* Add word64eqb_ZeqbGravatar Jason Gross2016-10-21
* Add fold_right_andb_true_iff_fold_right_and_TrueGravatar Jason Gross2016-10-19
* Fix broken [firstorder auto with *] >:-(Gravatar Jason Gross2016-10-19
* Add Tuple.map2Gravatar Jason Gross2016-10-19
* Fix for Coq 8.5, 8.5pl1Gravatar Jason Gross2016-10-18
* Add more simplify lemmas to ZUtilGravatar Jason Gross2016-10-17
* Add more simplify lemmas to ZUtilGravatar Jason Gross2016-10-17
* Add ZUtil lemmaGravatar Jason Gross2016-10-17
* refactor scalar multiplication thoery, implement SRepERepMulGravatar Andres Erbsen2016-10-12
* integrate bitwise operationsGravatar Andres Erbsen2016-10-12
* generalize equiv relations in Util.Option and EdDSARepChangeGravatar Andres Erbsen2016-10-12
* Generalize and simplify cast_word_reflGravatar Jason Gross2016-10-12
* word manipulation functions for secret key formatting (#74)Gravatar Andres Erbsen2016-10-12
* specialize_by: only specialize arguments of type [Prop]Gravatar Andres Erbsen2016-10-10
* specialize_by: explicitly maintain transparencyGravatar Andres Erbsen2016-10-10
* Ed25519: add basepoint and prove most EdDSA preconditionsGravatar Andres Erbsen2016-10-10
* Decidable: add [Z] and [nat] inequalitiesGravatar Andres Erbsen2016-10-10
* Fix compatibility with sigT notationGravatar Jason Gross2016-10-10
* Make Ztestbit_fullGravatar Jason Gross2016-10-09
* Fix Ztestbit_full databaseGravatar Jason Gross2016-10-09
* Fix shiftr_spec_fullGravatar Jason Gross2016-10-09
* Add more to Ztestbit_fullGravatar Jason Gross2016-10-09
* Add a Ztestbit_full databaseGravatar Jason Gross2016-10-09
* Stronger Ztestbit, convert_to_ztestbitGravatar Jason Gross2016-10-07
* More zsimplify lemmas, stronger ZtestbitGravatar Jason Gross2016-10-07
* Add eta_expand to Prod.vGravatar Jason Gross2016-10-07
* Weaken hyps of lor_range, add it to zarithGravatar Jason Gross2016-10-07
* Moved lemma to ZUtil and added an extra lemma jgross neededGravatar jadep2016-10-06
* Add testbit_add_shiftl_fullGravatar Jason Gross2016-10-06
* Use zutil_arith for side-conditions in testbitGravatar Jason Gross2016-10-06
* Add Z.pow_le_mono_{r,l} to zarithGravatar Jason Gross2016-10-06
* Add a lemma to Ztestbit about large indicesGravatar Jason Gross2016-10-06
* More zsimplify lemmasGravatar Jason Gross2016-10-04
* Add Zplus_minus to zsimplifyGravatar Jason Gross2016-10-04
* Weaken hyps of zutil lemmaGravatar Jason Gross2016-10-04
* Add a variant of add_shift_modGravatar Jason Gross2016-10-04
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
* Add Zmult_lt_compat_r to zarithGravatar Jason Gross2016-10-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 05:59:25 +0000