diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-15 21:21:35 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-16 14:35:53 -0500 |
| commit | 804189588135ba5e35f4fc4287f12b4179653620 (patch) | |
| tree | aed229afada2dfaf1acc93889a12c25da7c4ea2f /src/Specific/GF25519Reflective.v | |
| parent | f680d5ce3246f7415d480f5290f479cede90dacf (diff) | |
Split fixedpoint in interpf
Diffstat (limited to 'src/Specific/GF25519Reflective.v')
| -rw-r--r-- | src/Specific/GF25519Reflective.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/GF25519Reflective.v b/src/Specific/GF25519Reflective.v index a7ca684fb..1acef4e06 100644 --- a/src/Specific/GF25519Reflective.v +++ b/src/Specific/GF25519Reflective.v @@ -54,7 +54,7 @@ Declare Reduction asm_interp Z.interp_op Z.interp_base_type Z.Syntax.interp_op Z.Syntax.interp_base_type mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize - Interp interp interp_flat_type interpf interp_flat_type fst snd]. + Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. Ltac asm_interp := cbv beta iota delta [id |