aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmblock.v
diff options
context:
space:
mode:
authorJustus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>2020-07-07 10:01:29 +0200
committerJustus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>2020-07-07 10:01:29 +0200
commit8d9579bc41d08819dbe053e137fe1abe0c5928d8 (patch)
treec4c1cdd2e5871d9ef4a4520a72545ac64c884164 /aarch64/Asmblock.v
parent840899319d3a19269a6afe6f60e3a43d58647865 (diff)
downloadcompcert-kvx-8d9579bc41d08819dbe053e137fe1abe0c5928d8.tar.gz
compcert-kvx-8d9579bc41d08819dbe053e137fe1abe0c5928d8.zip
Remove out-of-date comment
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 *)