aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Preliminary support: conditional sub as primitiveGravatar Jason Gross2016-11-06
* Add syntactic tuplesGravatar Jason Gross2016-11-06
* Add functions for [tuple (option _) _]Gravatar Jason Gross2016-11-06
* Add support for dependent reificationGravatar Jason Gross2016-11-06
* Work around broken evars in 8.4Gravatar Jason Gross2016-11-06
* More partial proofsGravatar Jason Gross2016-11-06
* Prove inversion principles for bounded wordsGravatar Jason Gross2016-11-06
* Plug in boundedness proofsGravatar Jason Gross2016-11-05
* Add better bounded lemmas to reified thingsGravatar Jason Gross2016-11-05
* Add eta-expansion in GF25519BoundedCommon.vGravatar Jason Gross2016-11-05
* Add proofs about boundedness to GF25519Reflective/Common.vGravatar Jason Gross2016-11-05
* Add unfold_is_boundedGravatar Jason Gross2016-11-05
* Add related_word64_boundsi'Gravatar Jason Gross2016-11-05
* Add code for overflow check (disabled bc freeze)Gravatar Jason Gross2016-11-05
* Split off some things from InterpretationsGravatar Jason Gross2016-11-05
* Fix implicit argumentsGravatar Jason Gross2016-11-05
* Remove pasted code that shouldn't've been in a fileGravatar Jason Gross2016-11-05
* Add proj1_from_option2Gravatar Jason Gross2016-11-05
* Fix implicitsGravatar Jason Gross2016-11-05
* Fix a proof broken by previous commitGravatar Jason Gross2016-11-05
* Another projection functionGravatar Jason Gross2016-11-05
* Z.ltb_to_lt now works in the goal, tooGravatar Jason Gross2016-11-05
* Add reflect_iff_gen to Bool.vGravatar Jason Gross2016-11-05
* More judgmental unification in Z.InterpretationsGravatar Jason Gross2016-11-05
* Add proj_option2 to Z.InterpretationsGravatar Jason Gross2016-11-05
* Work around a bug in 8.4 vm_computeGravatar Jason Gross2016-11-05
* Fix implicits of Let for 8.4Gravatar Jason Gross2016-11-04
* put EdDSA encoding sign bit at the MSBGravatar Andres Erbsen2016-11-04
* fix extraction directives -- tested enc((l+1)B)=enc(B)Gravatar Andres Erbsen2016-11-03
* separate Ed25519Extraction.v, add extraction to MakefileGravatar Andres Erbsen2016-11-03
* Shove Z.Interpretations into closer alignmentGravatar Jason Gross2016-11-03
* fix Word64 constants for extraction, check in more extraction directivesGravatar Andres Erbsen2016-11-03
* Rearrangement to different judgmentally equal termsGravatar Jason Gross2016-11-03
* Add more projections in interpretationsGravatar Jason Gross2016-11-03
* Fix 8.4 build partiallyGravatar Jason Gross2016-11-03
* Add more interpretation thingsGravatar Jason Gross2016-11-03
* Fix buildGravatar Jason Gross2016-11-03
* More relatednessGravatar Jason Gross2016-11-03
* Make apply things go through interp_flat_typeGravatar Jason Gross2016-11-03
* Make apply things go through interp_flat_typeGravatar Jason Gross2016-11-03
* Versions of [Apply] that guarantee flat thingsGravatar Jason Gross2016-11-03
* Add more relatedness thingsGravatar Jason Gross2016-11-03
* Make [freeze] proofs consider machine integer width and hard input bounds sep...Gravatar jadep2016-11-03
* Fix bounds that were reversedGravatar Jason Gross2016-11-03
* Fix Not_found exception in 8.4Gravatar Jason Gross2016-11-03
* Clean up fe25519_word64ize, give examplesGravatar Jason Gross2016-11-02
* fix and prove ERepDec_correctGravatar Andres Erbsen2016-11-02
* add type-compatible SHA512 wrapperGravatar Andres Erbsen2016-11-02
* Fix divergence of Ltac match in 8.4Gravatar Jason Gross2016-11-02
* Fix diverging Qed in 8.5{,pl1} ([f_equal] is broken)Gravatar Jason Gross2016-11-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 16:56:08 +0000