diff options
| author |  Robert Sloan <varomodt@google.com> | 2016-10-13 11:51:48 -0700 |
|---|---|---|
| committer | Robert Sloan <varomodt@google.com> | 2016-10-13 11:51:48 -0700 |
| commit | 80c7c997affc5b3cfccfa5fa96b05ac77ab8a243 (patch) | |
| tree | c1186ac06e0fb43a38147c295bb763408d47c263 /src/Assembly/Pipeline.v | |
| parent | f33a97192cf426a4e0aa11ae2639b881ae1abc51 (diff) | |
Minor refactors waiting for the code generation to finish
Diffstat (limited to 'src/Assembly/Pipeline.v')
| -rw-r--r-- | src/Assembly/Pipeline.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index 68bb5f452..da1bf84ac 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -80,7 +80,7 @@ Module GF25519. { r: @HL.expr Z (@interp_type Z) ResultType | HL.interp (E := ZEvaluable) (t := ResultType) r = ge25519_add' P Q }. - Proof. Admitted. (* + Proof. vm_compute in P, Q; repeat match goal with | [x:?T |- _] => @@ -103,7 +103,7 @@ Module GF25519. interp_type interp_binop HL.interp Z.land ZEvaluable eadd esub emul eshiftr eand]. reflexivity. - Defined. *) + Defined. Definition ge25519_ast (P Q: @interp_type Z ResultType) := proj1_sig (ge25519_ast' P Q). |