Edit some TODOs

theories/algebra/to_agree.v

@@ -4,7 +4,6 @@ Require Import iris.prelude.options.
 
 (** [to_agree] of a [gmap] *)
 (* TODO: MOVE *)
-(* TODO: naming is a mess *)
 Section to_agree.
 Context `{Countable K} {A: Type}.
 

theories/logic/invariants.v

@@ -6,7 +6,9 @@ From gpfsl.base_logic Require Export vprop.
 Require Import iris.prelude.options.
 
 (** Lifting of Iris invariants to vProp *)
-(* TODO: defined general invariants. See https://gitlab.mpi-sws.org/iris/iris/-/issues/420 *)
+(* TODO: at least lift to monPred of iProp *)
+(* TODO: define general invariants.
+  See https://gitlab.mpi-sws.org/iris/iris/-/issues/420 *)
 Section defs.
 Context `{invGS Σ}.
 Notation vProp := (vProp Σ).