From 8dfd1db5c496821b8cb94ce7b121e4b9bba3d265 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 7 Dec 2020 23:51:58 +0100
Subject: Some cleanup in todos

---
 aarch64/Asmgenproof.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'aarch64/Asmgenproof.v')

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index eac406a1..793d94f9 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -807,7 +807,6 @@ Proof.
   - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity).
 Qed.
 
-(* TODO *)
 Lemma exec_basic_dont_move_PC bi rs m rs' m': forall
   (BASIC: exec_basic lk ge bi rs m = Next rs' m'),
   rs PC = rs' PC.
@@ -1660,7 +1659,6 @@ Proof.
     + destruct H.
 Qed.
 
-(* TODO *)
 Lemma no_label_in_basic_inst: forall a lbl x,
   basic_to_instruction a = OK x -> Asm.is_label lbl x = false.
 Proof.
-- 
cgit