Full automation for relevant parts of pseudo conversion except lets

1 files changed, 8 insertions, 5 deletions

diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index e7e9b0c7d..dbd46b1b4 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -50,13 +50,16 @@ Module EvalUtil.
 
   Definition highBits {n} (m: nat) (x: word n) := snd (break m x).
 
-  Definition evalDualOp {n} (duo: DualOp) (x y: word n): word n * word n.
-    refine match duo with
-    | Mult => (x ^* y,
-        @extend _ n _ ((highBits (n/2) x) ^* (highBits (n/2) y)))
-    end; abstract omega.
+  Definition multHigh {n} (x y: word n): word n.
+    refine (@extend _ n _ ((highBits (n/2) x) ^* (highBits (n/2) y)));
+      abstract omega.
   Defined.
 
+  Definition evalDualOp {n} (duo: DualOp) (x y: word n) :=
+    match duo with
+    | Mult => (x ^* y, multHigh x y)
+    end.
+
   Definition evalRotOp {b} (ro: RotOp) (x: word b) (n: nat) :=
     match ro with
     | Shl => NToWord b (N.shiftl_nat (wordToN x) n)