aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Add [f] to things that use [exprf] or [flat_type]Gravatar Jason Gross2016-10-31
* Implicits for SmartVarMapTGravatar Jason Gross2016-10-31
* Make it so that changing the list of wire bounds doesn't break the buildGravatar Jason Gross2016-10-31
* Add SmartVarMapTGravatar Jason Gross2016-10-31
* Revert "Switch from word to Z"Gravatar Jason Gross2016-10-31
* Switch from word to ZGravatar Jason Gross2016-10-31
* Switch to reflective bounded word in Ed25519Gravatar Jason Gross2016-10-31
* Safer definitions of shl, shrGravatar Jason Gross2016-10-31
* Fix a typo making word calculations wrongGravatar Jason Gross2016-10-31
* Use sigma types to fix extractionGravatar Jason Gross2016-10-31
* Silence a warningGravatar Jason Gross2016-10-31
* Significantly faster wordToN, I hopeGravatar Jason Gross2016-10-31
* Add src/Specific/GF25519Reflective.vGravatar Jason Gross2016-10-31
* Interpret syntax with Let_InGravatar Jason Gross2016-10-31
* Also construct relatedness proofs in reifiedGravatar Jason Gross2016-10-30
* Fix tactic notation scope in the 8.5 buildGravatar Jason Gross2016-10-30
* Fix for 8.5 build?Gravatar Jason Gross2016-10-30
* Proved eq_enc_E_iffGravatar jadep2016-10-30
* Fix some subtleties with equalities in point encodingsGravatar jadep2016-10-30
* Added new algebra lemmaGravatar jadep2016-10-30
* Remove an [About]Gravatar Jason Gross2016-10-30
* Renaming in Reflection/Z/Interpretations.v, admitted rel lemmasGravatar Jason Gross2016-10-30
* Switch to a faster way of proving wfGravatar 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
* Generalize interp_flat_type_rel_pointwise2 a bitGravatar Jason Gross2016-10-30
* Minor changes to GF25519 reflectiveGravatar Jason Gross2016-10-30
* Add PartiallyReifiedPropGravatar Jason Gross2016-10-30
* Add reification of various operationsGravatar Jason Gross2016-10-30
* Add initial work on reifying GF25519 stuffGravatar Jason Gross2016-10-30
* Handle 4 arguments in ReifyGravatar Jason Gross2016-10-30
* remove commented-out lemmaGravatar jadep2016-10-30
* revived accidentally deleted lemmaGravatar jadep2016-10-30
* Revert "Premature optimization of [Reify_rhs]"Gravatar Jason Gross2016-10-30
* Premature optimization of [Reify_rhs]Gravatar Jason Gross2016-10-30
* Fix slowness in [Defined] after [Reify_rhs]Gravatar Jason Gross2016-10-30
* Make Z Reification handle correctness proofsGravatar Jason Gross2016-10-30
* Factor out prove_compile_correctGravatar Jason Gross2016-10-30
* Adjust arguments to InputSyntax.CompileGravatar Jason Gross2016-10-30
* Generalize Reify a bitGravatar Jason Gross2016-10-30
* Generalize InputSyntax.Compile_correctGravatar Jason Gross2016-10-30
* Factor Reify_rhs so that it's more reusableGravatar Jason Gross2016-10-30
* framework for l_order_BGravatar Andres Erbsen2016-10-30
* Minor reflective changesGravatar Jason Gross2016-10-30
* proved feSign_correctGravatar jadep2016-10-29
* proved Proper_feSignGravatar jadep2016-10-29
* Fix an infinite loopGravatar Jason Gross2016-10-29
* Add things like app_7 to GF25519BoundedCommonWord.vGravatar Jason Gross2016-10-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 02:43:47 +0000