diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 19:38:20 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 19:38:20 -0400 |
| commit | 5cb07f239f82528ba5422556f59294511326c2ad (patch) | |
| tree | b481712e4aa71a412ff1aec0f0b37bb51c09375d /src/Assembly/QhasmUtil.v | |
| parent | 7df5ed48ce1e16eebd4ec4cac9f057c65d40ae78 (diff) | |
Make Assembly modules 8.5-compatible
Diffstat (limited to 'src/Assembly/QhasmUtil.v')
| -rw-r--r-- | src/Assembly/QhasmUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v index f49d48573..1c5c6b807 100644 --- a/src/Assembly/QhasmUtil.v +++ b/src/Assembly/QhasmUtil.v @@ -48,7 +48,7 @@ Section Util. | _ => fun _ => left _ end eq_refl); abstract ( unfold c in *; unfold N.lt, N.ge; - rewrite _H in *; intuition; try inversion H). + rewrite e in *; intuition; try inversion H). Defined. Definition break {n} (m: nat) (x: word n): word m * word (n - m). |