Fix evalWordRangeOpt

2 files changed, 3 insertions, 1 deletions

diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v
index 823d05cfb..6a08a7d54 100644
--- a/src/Assembly/Evaluables.v
+++ b/src/Assembly/Evaluables.v
@@ -548,7 +548,7 @@ Section WordRange.
     | someRange low high _ _ => Some (range N low high)
     | applyBinOp rangeF wordF _ a b =>
       omap (evalWordRangeOpt a) (fun a' =>
-        omap (evalWordRangeOpt a) (fun b' =>
+        omap (evalWordRangeOpt b) (fun b' =>
           rangeF a' b'))
     end.
 
diff --git a/src/Experiments/SpecificCurve25519.v b/src/Experiments/SpecificCurve25519.v
index b5878825f..80f6ff3a6 100644
--- a/src/Experiments/SpecificCurve25519.v
+++ b/src/Experiments/SpecificCurve25519.v
@@ -118,6 +118,8 @@ Module Input.
 
   Definition ZInterp {t} E := @Interp Z ZEvaluable t E.
 
+  Definition WordInterp {n t} E := @Interp (word n) (@WordEvaluable n) t E.
+
   Definition RangeInterp {n t} E: @interp_type (option (Range N)) t :=
     typeMap evalWordRangeOpt (@Interp (@WordRangeOpt n) (@WordRangeOptEvaluable n) t E).