diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-06-06 11:31:33 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:43:38 -0400 |
| commit | 9ed91fb68aaf520b28e01c46aeddc33573677668 (patch) | |
| tree | 24053f820aed9dcd41aef48e8e59d646ceaa162f /src/Assembly/QhasmCommon.v | |
| parent | 8f2241042d26d94b138a6f2a51287dae413b7ec2 (diff) | |
Full pipeline working again
Diffstat (limited to 'src/Assembly/QhasmCommon.v')
| -rw-r--r-- | src/Assembly/QhasmCommon.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v index 21f846cb5..654f109f3 100644 --- a/src/Assembly/QhasmCommon.v +++ b/src/Assembly/QhasmCommon.v @@ -19,7 +19,7 @@ Inductive Width: nat -> Type := | W32: Width 32 | W64: Width 64. (* A constant value *) Inductive Const: nat -> Type := - | const: forall {n}, Width n -> word n -> Const n. + | constant: forall {n}, Width n -> word n -> Const n. (* A variable in any register *) Inductive Reg: nat -> Type := @@ -109,10 +109,10 @@ Definition memWidth {n m} (x: Mem n m): nat := n. Definition memLength {n m} (x: Mem n m): nat := m. Definition constValueW {n} (x: Const n): word n := - match x with | @const n _ v => v end. + match x with | @constant n _ v => v end. Definition constValueN {n} (x: Const n): nat := - match x with | @const n _ v => wordToNat v end. + match x with | @constant n _ v => wordToNat v end. Definition regName {n} (x: Reg n): nat := match x with | @reg n _ v => v end. |