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