aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* 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
* Handle Let_In in reificationGravatar Jason Gross2016-10-29
* Fix type reificationGravatar Jason Gross2016-10-29
* Also test 8.5pl3 on travisGravatar Jason Gross2016-10-29
* Finer grained type reificationGravatar Jason Gross2016-10-29
* Disable extraction in src/Assembly/GF25519.vGravatar Jason Gross2016-10-29
* Disable some printingGravatar Jason Gross2016-10-29
* prove Proper_SRepERepMulGravatar Andres Erbsen2016-10-29
* prove testbit_sub_pow2Gravatar Andres Erbsen2016-10-29
* More 8.4 fixesGravatar Jason Gross2016-10-29
* Fix for 8.4Gravatar Jason Gross2016-10-29
* Finish proof in src/Reflection/InlineWf.vGravatar Jason Gross2016-10-29
* Add more WfProofsGravatar Jason Gross2016-10-29
* Add InterpWfGravatar Jason Gross2016-10-28
* Add InterpWfRelGravatar Jason Gross2016-10-28
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
* 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
* Merge pull request #84 from mit-plv/rsloan-phoasGravatar Jason Gross2016-10-27
|\
* | prove admit about F.to_nat x mod mGravatar Andres Erbsen2016-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-03 17:18:58 +0000