aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly/PseudoConversion.v
diff options
context:
space:
mode:
authorGravatar Robert Sloan <varomodt@gmail.com>2016-06-22 19:38:20 -0400
committerGravatar Robert Sloan <varomodt@gmail.com>2016-06-22 19:38:20 -0400
commit5cb07f239f82528ba5422556f59294511326c2ad (patch)
treeb481712e4aa71a412ff1aec0f0b37bb51c09375d /src/Assembly/PseudoConversion.v
parent7df5ed48ce1e16eebd4ec4cac9f057c65d40ae78 (diff)
Make Assembly modules 8.5-compatible
Diffstat (limited to 'src/Assembly/PseudoConversion.v')
-rw-r--r--src/Assembly/PseudoConversion.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v
index 35f8e1e30..9c3fda2a0 100644
--- a/src/Assembly/PseudoConversion.v
+++ b/src/Assembly/PseudoConversion.v
@@ -174,7 +174,7 @@ Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
Some (ASeq
(AAssign (AConstInt (reg' a) (const' (natToWord _ O))))
(AWhile (CConst _ TLt (reg' a) (const' (natToWord _ e)))
- (ASeq fp (AOp (IOpConst Add (reg' a) (const' (natToWord _ 1)))))),
+ (ASeq fp (AOp (IOpConst IAdd (reg' a) (const' (natToWord _ 1)))))),
fr, madd a rM M', F')
| _ => None