aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* extraction: inline field operations into group operationsGravatar Andres Erbsen2016-11-14
* for i in *.json; do ./copy_bounds.sh $i; doneGravatar Jason Gross2016-11-14
* Add mulW_noinlineGravatar Jason Gross2016-11-14
* Proper_sqrtGravatar Andres Erbsen2016-11-13
* Proper_sqrt_3mod4 Proper_sqrt_5mod8Gravatar Andres Erbsen2016-11-13
* Don't copy bounds files if no argument is passedGravatar Jason Gross2016-11-13
* Add SpecificGen/GF*Gravatar Jason Gross2016-11-13
* Work around bug #5198 (broken tc resolution)Gravatar Jason Gross2016-11-12
* More 8.4pl2 fixesGravatar Jason Gross2016-11-12
* Fix for Coq 8.2Gravatar Jason Gross2016-11-12
* Fix for Coq 8.4pl2Gravatar Jason Gross2016-11-12
* Remove extra admitted lemmas in 8.4Gravatar Jason Gross2016-11-12
* Fixes for 8.4 (instantiate)Gravatar Jason Gross2016-11-12
* GF25519: add ErepAddGravatar Andres Erbsen2016-11-11
* GF25519: add optimized addition chainGravatar Andres Erbsen2016-11-11
* use @implicits in rewrite (8.4)Gravatar Andres Erbsen2016-11-11
* Proved postfreezeW_correct_and_boundedGravatar jadep2016-11-11
* Remove dead code in rebuild-reified.pyGravatar Jason Gross2016-11-11
* Begin filling in @JasonGross's stubsGravatar jadep2016-11-11
* Define word version of conditional subtractionGravatar jadep2016-11-11
* separate freeze into two partsGravatar jadep2016-11-11
* Fix reification of negGravatar Jason Gross2016-11-11
* Make [neg] a unary operation in reflectionGravatar Jason Gross2016-11-11
* Remove more conditional subtractGravatar Jason Gross2016-11-11
* Remove extra conditional subtract thingsGravatar Jason Gross2016-11-11
* Remove special code for reified conditional subGravatar Jason Gross2016-11-11
* 8.4-compatible universe handlingGravatar Jason Gross2016-11-11
* Remove 8.6 only syntaxGravatar Jason Gross2016-11-11
* Automatically generate code for field operations with different primesGravatar jadep2016-11-11
* Freeze stubsGravatar Jason Gross2016-11-11
* Lemmas about winit, wlastGravatar Rob Sloan2016-11-11
* prove last HList admitGravatar Andres Erbsen2016-11-11
* prove admits in Util.TupleGravatar Andres Erbsen2016-11-11
* [cbn] is 8.5 onlyGravatar Jason Gross2016-11-11
* Fix for Coq 8.4Gravatar Jason Gross2016-11-11
* Fix proofs broken by stronger preconditionsGravatar Jason Gross2016-11-11
* Most of the admits in Ed25519.vGravatar Rob Sloan2016-11-11
* extraction less slowGravatar Andres Erbsen2016-11-11
* Add Tuple and HList lemmasGravatar Jason Gross2016-11-10
* Work around looping in 8.4Gravatar Jason Gross2016-11-10
* More proof fixesGravatar Jason Gross2016-11-10
* Fix for 8.4Gravatar Jason Gross2016-11-10
* Minimize diff with master, fix some proofs that were brokenGravatar Jason Gross2016-11-10
* Hint Rewrite is section-local; move to top-levelGravatar Jason Gross2016-11-10
* Remove WordizeUtil dependency from WordUtilGravatar Rob Sloan2016-11-09
* Merge with masterGravatar Rob Sloan2016-11-09
|\
| * Fix for 8.4Gravatar Jason Gross2016-11-09
| * Switch to accurate bounds for lorGravatar Jason Gross2016-11-09
* | Rebase + remove WordizeUtil dependency from Z/InterpretationsGravatar Rob Sloan2016-11-09
|\ \
| | * Remove last admitted lemma in src/Reflection/Z/Interpretations/Relations.vGravatar Jason Gross2016-11-09
| |/
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 01:31:28 +0000