aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* 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
* 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
* | proved last admit (Proper_feEnc) in Experiments/Ed25519Gravatar jadep2016-10-27
* | proved an admit (eq_enc_S_iff) in Ed25519.vGravatar jadep2016-10-27
* | Add Inline importGravatar Jason Gross2016-10-27
* | Add {un,}curry_wire_digitsGravatar Jason Gross2016-10-27
* | CompleteEdwardsCurve.ExtendedCoordinates: remove admitted lift_homomorphism l...Gravatar Andres Erbsen2016-10-27
* | Add {un,}curry_{bin,un}op_fe25519Gravatar Jason Gross2016-10-27
* | Add length_fe25519Gravatar Jason Gross2016-10-27
* | Fix implicit status of curryGravatar Jason Gross2016-10-27
* | Add curry and uncurry to tupleGravatar Jason Gross2016-10-27
* | Add syntax and reification for the ops in GF25519Gravatar Jason Gross2016-10-27
* | Fix a missing import in previous commitGravatar Jason Gross2016-10-27
* | Factor out cmov{l,ne} and negGravatar Jason Gross2016-10-27
* | PHOAS notation fixupsGravatar Jason Gross2016-10-27
* | Make it easier to export only phoas notationsGravatar Jason Gross2016-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 19:51:05 +0000