diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-08-24 21:37:24 -0700 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-08-24 21:37:24 -0700 |
| commit | 8233eba820c0108dbc6390c8871857e39f3fbf08 (patch) | |
| tree | 0931c7ae8bf20e36ad7a5875c99ee68e34898821 /src/Experiments | |
| parent | 9c7493d9d9edcd7038f6e4a60fcfd1ddbc13a286 (diff) | |
Finishing tactical machinery for bound-computing
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/SpecificCurve25519.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Experiments/SpecificCurve25519.v b/src/Experiments/SpecificCurve25519.v index 10453c7f2..627cec758 100644 --- a/src/Experiments/SpecificCurve25519.v +++ b/src/Experiments/SpecificCurve25519.v @@ -303,8 +303,8 @@ Module Output. match e with | LetBinop _ _ op a b _ eC => let x := interp_binop op (interp_arg a) (interp_arg b) in interp (eC x) - | Return _ a => interp_arg a - end. + | Return _ a => interp_arg a + end. Definition Interp {t} (E:Expr t) : interp_type t := interp (E T). End Language. |