| Commit message (Expand) | Author | Age |
* | Add InterpWfRel | Jason Gross | 2016-10-28 |
* | Add interp_type_gen_rel_pointwise2, *_gen => * | Jason Gross | 2016-10-28 |
* | Some work on proofs in src/Reflection/Z/Interpretations.v | Jason Gross | 2016-10-27 |
* | Add some rewrites and admitted lemmas | Jason Gross | 2016-10-27 |
* | Add beginnings of various interpretations of expression trees | Jason Gross | 2016-10-27 |
* | Add {push,pull}_Zof_N hint db to ZUtil | Jason Gross | 2016-10-27 |
* | Merge pull request #84 from mit-plv/rsloan-phoas | Jason Gross | 2016-10-27 |
|\ |
|
* | | prove admit about F.to_nat x mod m | Andres Erbsen | 2016-10-27 |
* | | proved last admit (Proper_feEnc) in Experiments/Ed25519 | jadep | 2016-10-27 |
* | | proved an admit (eq_enc_S_iff) in Ed25519.v | jadep | 2016-10-27 |
* | | Add Inline import | Jason Gross | 2016-10-27 |
* | | Add {un,}curry_wire_digits | Jason Gross | 2016-10-27 |
* | | CompleteEdwardsCurve.ExtendedCoordinates: remove admitted lift_homomorphism l... | Andres Erbsen | 2016-10-27 |
* | | Add {un,}curry_{bin,un}op_fe25519 | Jason Gross | 2016-10-27 |
* | | Add length_fe25519 | Jason Gross | 2016-10-27 |
* | | Fix implicit status of curry | Jason Gross | 2016-10-27 |
* | | Add curry and uncurry to tuple | Jason Gross | 2016-10-27 |
* | | Add syntax and reification for the ops in GF25519 | Jason Gross | 2016-10-27 |
* | | Fix a missing import in previous commit | Jason Gross | 2016-10-27 |
* | | Factor out cmov{l,ne} and neg | Jason Gross | 2016-10-27 |
* | | PHOAS notation fixups | Jason Gross | 2016-10-27 |
* | | Make it easier to export only phoas notations | Jason Gross | 2016-10-27 |
* | | add wf, not only rel_wf, to MapInterpWf | Jason Gross | 2016-10-27 |
* | | Add WfRelReflective | Jason Gross | 2016-10-27 |
* | | Factor WfReflective through WfReflectiveGen | Jason Gross | 2016-10-27 |
* | | removed now irrelevant commented-out code | jadep | 2016-10-27 |
* | | convert feEnc correctness proof to bounded type | jadep | 2016-10-27 |
* | | finished feEnc correctness | jadep | 2016-10-27 |
* | | most of feEnc correctness proof | jadep | 2016-10-27 |
* | | Slightly loosen freeze preconditions (in particular, I had failed to properly... | jadep | 2016-10-27 |
* | | add extra convenience lemmas about boundedness of convert | jadep | 2016-10-27 |
* | | removed lingering TODO | jadep | 2016-10-27 |
* | | Implicits for reflect_wfT | Jason Gross | 2016-10-27 |
* | | Add WfReflectiveGen | Jason Gross | 2016-10-27 |
* | | Move interp_flat_type_gen_rel_pointwise2 to Syntax | Jason Gross | 2016-10-27 |
* | | Add Wf proofs about MapInterp | Jason Gross | 2016-10-27 |
* | | Add arguments to mapf_interp_flat_type_gen | Jason Gross | 2016-10-27 |
* | | Add implicits to interp_flat_type_gen_rel_pointwise2 | Jason Gross | 2016-10-27 |
* | | Change the argument implicits on rel_wff | Jason Gross | 2016-10-27 |
| * | Merge branch 'master' into rsloan-phoas | Jason Gross | 2016-10-27 |
| |\
| |/
|/| |
|
* | | Revert change to [nsatz] (it was making Coq run out of memory) | Jason Gross | 2016-10-27 |
| * | Merge branch 'master' into rsloan-phoas | Jason Gross | 2016-10-27 |
| |\ |
|
* | | | Simplify proof of proj1_fe25519_encode | Jason Gross | 2016-10-27 |
* | | | Add lemmas about GF25519BoundedCommon.{encode,decode} | Jason Gross | 2016-10-27 |
| |/
|/| |
|
| * | Fixes for Coq 8.4 | Jason Gross | 2016-10-27 |
| * | Strip function extensionality, enable printing of sub, mul, opp, freeze | Jason Gross | 2016-10-27 |
* | | Various fixes in alternative nsatz | Jason Gross | 2016-10-27 |
| * | Tactics to manually remove Z.to/of_N and such | Robert Sloan | 2016-10-26 |
* | | Handle folded [not] in nsatz_strip_fractions | Jason Gross | 2016-10-26 |
* | | Split inequalities before specializing | Jason Gross | 2016-10-26 |