aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmblock.v
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/Asmblock.v')
-rw-r--r--aarch64/Asmblock.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index b61288e9..e0815890 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -285,7 +285,6 @@ Inductive arith_p : Type :=
.
(* Arithmetic instructions with conditional execution *)
-(* TODO matching case in ar_instruction *)
Inductive arith_c_p : Type :=
(** Conditional data processing *)
| Pcset (**r set to 1/0 if cond is true/false *)