diff options
Diffstat (limited to 'powerpc/Machregs.v')
| -rw-r--r-- | powerpc/Machregs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index d0f7cf4..88b70c1 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -29,7 +29,7 @@ Require Import AST. The type [mreg] does not include special-purpose or reserved machine registers such as the stack pointer and the condition codes. *) -Inductive mreg: Set := +Inductive mreg: Type := (** Allocatable integer regs *) | R3: mreg | R4: mreg | R5: mreg | R6: mreg | R7: mreg | R8: mreg | R9: mreg | R10: mreg |