aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Fix for 8.5 build?Gravatar Jason Gross2016-10-30
* Add trueify to src/Util/PartiallyReifiedProp.vGravatar Jason Gross2016-10-30
* Add to_prop_and_reified_PropGravatar Jason Gross2016-10-30
* Add break_innermost_matchGravatar Jason Gross2016-10-30
* Fix a loop in PartiallyReifiedPropGravatar Jason Gross2016-10-30
* Add PartiallyReifiedPropGravatar Jason Gross2016-10-30
* prove Proper_SRepERepMulGravatar Andres Erbsen2016-10-29
* prove testbit_sub_pow2Gravatar Andres Erbsen2016-10-29
* Some work on proofs in src/Reflection/Z/Interpretations.vGravatar Jason Gross2016-10-27
* Add some rewrites and admitted lemmasGravatar Jason Gross2016-10-27
* Add beginnings of various interpretations of expression treesGravatar Jason Gross2016-10-27
* Add {push,pull}_Zof_N hint db to ZUtilGravatar Jason Gross2016-10-27
* prove admit about F.to_nat x mod mGravatar Andres Erbsen2016-10-27
* Fix implicit status of curryGravatar Jason Gross2016-10-27
* Add curry and uncurry to tupleGravatar Jason Gross2016-10-27
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 15:18:37 +0000