aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* 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
* | 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
* | add wf, not only rel_wf, to MapInterpWfGravatar Jason Gross2016-10-27
* | Add WfRelReflectiveGravatar Jason Gross2016-10-27
* | Factor WfReflective through WfReflectiveGenGravatar Jason Gross2016-10-27
* | removed now irrelevant commented-out codeGravatar jadep2016-10-27
* | convert feEnc correctness proof to bounded typeGravatar jadep2016-10-27
* | finished feEnc correctnessGravatar jadep2016-10-27
* | most of feEnc correctness proofGravatar jadep2016-10-27
* | Slightly loosen freeze preconditions (in particular, I had failed to properly...Gravatar jadep2016-10-27
* | add extra convenience lemmas about boundedness of convertGravatar jadep2016-10-27
* | removed lingering TODOGravatar jadep2016-10-27
* | Implicits for reflect_wfTGravatar Jason Gross2016-10-27
* | Add WfReflectiveGenGravatar Jason Gross2016-10-27
* | Move interp_flat_type_gen_rel_pointwise2 to SyntaxGravatar Jason Gross2016-10-27
* | Add Wf proofs about MapInterpGravatar Jason Gross2016-10-27
* | Add arguments to mapf_interp_flat_type_genGravatar Jason Gross2016-10-27
* | Add implicits to interp_flat_type_gen_rel_pointwise2Gravatar Jason Gross2016-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 07:41:06 +0000