aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* 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
* Define carry_opp in terms of carry_subGravatar Jason Gross2016-10-19
* Add opt versions of add, sub, oppGravatar Jason Gross2016-10-19
* Fix for change in precedence of <-> vs -> in 8.4/8.5Gravatar Jason Gross2016-10-19
* Fix out of memory error for 8.5,8.5pl1Gravatar Jason Gross2016-10-19
* Work around out of memory error in 8.5, 8.5pl1Gravatar Jason Gross2016-10-18
* Work around bug #5149 in 8.6 (broken subst, evars)Gravatar Jason Gross2016-10-18
* Fix for Coq 8.5, 8.5pl1Gravatar Jason Gross2016-10-18
* Fix for Coq 8.4 evar propogationGravatar Jason Gross2016-10-18
* Fix missing importsGravatar Jason Gross2016-10-17
* Remove broken importsGravatar Jason Gross2016-10-17
* Rename and clean up exponent codeGravatar Jason Gross2016-10-17
* Remove admits with the help of AndresGravatar Jason Gross2016-10-17
* Fill in more proofsGravatar Jason Gross2016-10-17
* Initial work on exponent field as ZGravatar Jason Gross2016-10-17
* Be more hesitant to [pose proof E.char_gt_2]Gravatar Jason Gross2016-10-17
* Don't let [tauto] destruct [Equivalence] in PEGravatar Jason Gross2016-10-17
* Fix for 8.4 unification being unhappy in Ed25519 (nats are terrible)Gravatar Jason Gross2016-10-17
* Various Ed25519 8.4 fixesGravatar Jason Gross2016-10-17
* Fix location of code in previous commitGravatar Jason Gross2016-10-17
* Add field by isomorphismGravatar Jason Gross2016-10-17
* 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
* Fix a proofGravatar Jason Gross2016-10-16
* Don't inline as much in ZBoundedZGravatar Jason Gross2016-10-16
* Add Z as ZBoundedGravatar Jason Gross2016-10-16
* Actually fix the exponential blowup (hopefully)Gravatar Jason Gross2016-10-14
* Fix a typo in the previous commitGravatar Jason Gross2016-10-14
* Fix exponential blowup in some doubling opsGravatar Jason Gross2016-10-14
* Work around bug 5401 (bad let '(x, y))Gravatar Jason Gross2016-10-13
* Revert "Eta-expand pairs in Eta.v"Gravatar Jason Gross2016-10-13
* Eta-expand pairs in Eta.vGravatar Jason Gross2016-10-13
* Unfold more things in etaGravatar Jason Gross2016-10-13
* Fix for Coq 8.4Gravatar Jason Gross2016-10-13
* Add src/BoundedArithmetic/Eta.vGravatar Jason Gross2016-10-13
* refactor scalar multiplication thoery, implement SRepERepMulGravatar Andres Erbsen2016-10-12
* Fixed naming issueGravatar jadep2016-10-12
* defined sign operation on field elementsGravatar jadep2016-10-12
* Fixing merge conflictGravatar jadep2016-10-12
* Clean up ge_modulus definition in SpecificGravatar jadep2016-10-12
* Added top-level modulus comparison operation so field-element decoding can re...Gravatar jadep2016-10-12
* integrate bitwise operationsGravatar Andres Erbsen2016-10-12
* generalize equiv relations in Util.Option and EdDSARepChangeGravatar Andres Erbsen2016-10-12
* remove Experiments.EncodingLemmas (superseded by Jade's recent work)Gravatar Andres Erbsen2016-10-12
* Add Ed25519 to _CoqProjectGravatar Jason Gross2016-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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 21:32:29 +0000