diff options
Diffstat (limited to 'backend/PPC.v')
| -rw-r--r-- | backend/PPC.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/PPC.v b/backend/PPC.v index 37f882b..3aa4ec4 100644 --- a/backend/PPC.v +++ b/backend/PPC.v @@ -286,7 +286,7 @@ lbl: .long 0x43300000, 0x00000000 Definition code := list instruction. Definition fundef := AST.fundef code. -Definition program := AST.program fundef. +Definition program := AST.program fundef unit. (** * Operational semantics *) |