aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Expand)AuthorAge
* Fix divergence of Ltac match in 8.4Gravatar Jason Gross2016-11-02
* improve some fragile proofs (built on 8.4)Gravatar Andres Erbsen2016-11-02
* Add ZUtil.Z.log2_ones_lt_nonnegGravatar Jason Gross2016-11-02
* Add more ZUtilGravatar Jason Gross2016-11-02
* Add ZUtil lemmaGravatar Jason Gross2016-11-02
* Add ZUtil lemmaGravatar Jason Gross2016-11-02
* Add a ZUtil lemmaGravatar Jason Gross2016-11-02
* Change hlist implicit statusGravatar Jason Gross2016-11-01
* Move hlist to new fileGravatar Jason Gross2016-11-01
* Fix a typo in the previous commitGravatar Jason Gross2016-11-01
* Generalize hlistGravatar Jason Gross2016-11-01
* Add hlist to tupleGravatar Jason Gross2016-11-01
* Add some interpretations things, speed up proofs in Ed25519Gravatar Jason Gross2016-10-31
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 06:38:36 +0000