Remove TODO item

The code is now SPARK-compliant and can be analyzed using GPL 2017.

Signed-off-by: Adrian-Ken Rueegsegger <ken@codelabs.ch>

diff --git a/TODO.md b/TODO.md
index d3f53e1d5a449486ef16a557a635f1270dcdb582..fbce78f90b5fa2f08f5bc782eb4d565af90e3d9d 100644 (file)
--- a/TODO.md
+++ b/TODO.md
@@ -9,9 +9,6 @@ Document the build process for a stand-alone library (utilizing
 
 ## SPARK
 
-* Rework the code to be valid SPARK (no errors from `gnatprove
-  -m check`)
-
 * Prove absence of runtime errors