diff --git a/elpi/annot.elpi b/elpi/annot.elpi
index cf8c230..619edb7 100644
--- a/elpi/annot.elpi
+++ b/elpi/annot.elpi
@@ -74,8 +74,6 @@ sub-type (app [F|Xs]) (app [F'|Xs']) :-
 % SubConv
 sub-type X X :- (name X ; X = global _ ; X = pglobal _ _), !.
 sub-type X Y :- coq.unify-eq X Y _.
-% TODO: perform controlled reduction
-% and extend implementation to fix, match, etc.
 sub-type X Y :- coq.error "annot.sub-type:" X "vs" Y.
 
 % syntactic term equality, taking care of adding annotation equalities in the constraint graph
@@ -100,7 +98,6 @@ eq _ _ :- fail.
 % of the output type of T, as an option basically returning some (A,B) for an output type PType A B,
 % and none for output types that are not sorts, because it means values of type T are not type
 % constructors, so their translation will be made at class (0,0)
-% TODO: duplicate code with type->class in param-class.elpi?
 pred classes i:term, o:list param-class, o:option param-class.
 classes T Cs' Out :-
   all-classes T Cs,
@@ -121,7 +118,7 @@ all-classes (app L) Cs :- !,
 all-classes X [] :- (name X ; X = global _ ; X = pglobal _ _), !.
 all-classes X _ :- coq.error "all-classes:" X.
 
-% TODO: discuss limitations
+% output class of a term
 pred out-class i:term, o:option param-class.
 out-class (app [pglobal (const PType) _, M, N]) (some C) :- trocq.db.ptype PType, !,
   cstr.univ-link C M N.
@@ -132,6 +129,5 @@ out-class (app [F|Xs]) Out :- !,
   if (App = app [F|Xs]) (Out = none) (out-class App Out).
 out-class X none :- (name X ; X = global _ ; X = pglobal _ _), !.
 out-class X _ :- coq.error "out-class:" X.
-% constant applications convertible to terms having a sort as output are not supported
 
 } % annot
diff --git a/elpi/constraints/constraint-graph.elpi b/elpi/constraints/constraint-graph.elpi
index 5e9d94b..db3aee1 100644
--- a/elpi/constraints/constraint-graph.elpi
+++ b/elpi/constraints/constraint-graph.elpi
@@ -80,8 +80,7 @@ pred add-dep-gref
 add-dep-gref ID GR T Tm' GRR IDs (constraint-graph G) (constraint-graph G') :-
   % the classes C_i (IDs) are not really "higher" than the output class C (ID)
   % here, higher is a way to say that they must be instantiated later than the output class
-  % TODO: rename utility functions to add-earlier-node / add-later-node?
-  util.map.update ID (internal.add-higher-node (node.var (ct.gref GR T Tm' GRR) IDs)) G G1,
+  util.map.update ID (internal.add-higher-node (node.var (ct.gref GR T GR' GRR) IDs)) G G1,
   std.fold IDs G1 (id\ g\ g'\
     util.map.update id (internal.add-lower-node (node.var (ct.gref _ _ _ _) [ID])) g g')
       G'.
diff --git a/elpi/param.elpi b/elpi/param.elpi
index 5e2b8df..5a035e5 100644
--- a/elpi/param.elpi
+++ b/elpi/param.elpi
@@ -227,7 +227,6 @@ type wsuspend (term -> term) -> (term -> term) -> weakening.
 
 % generate the weakening function from a type to a sub-type
 % cf definition of weakening in the paper
-% TODO: document suspend
 pred weakening i:term, i:term, o:weakening.
 weakening (app [pglobal (const PType) _, M, N]) (app [pglobal (const PType) _, M', N']) W :-
   trocq.db.ptype PType, !,
diff --git a/elpi/util.elpi b/elpi/util.elpi
index 569c3f8..8dc57d2 100644
--- a/elpi/util.elpi
+++ b/elpi/util.elpi
@@ -14,7 +14,6 @@
 % utility predicates
 % -----------------------------------------------------------------------------
 
-% TODO: document
 pred do-not-fail.
 :before "term->gref:fail"
 coq.term->gref _ _ :- do-not-fail, !, false.
diff --git a/theories/Param.v b/theories/Param.v
index 8ba2540..e13ee65 100644
--- a/theories/Param.v
+++ b/theories/Param.v
@@ -29,7 +29,6 @@ From Trocq.Elpi.constraints Extra Dependency "constraints.elpi" as constraints.
 Set Universe Polymorphism.
 Unset Universe Minimization ToSet.
 
-(* TODO: dead code? *)
 Elpi Command genpparam.
 Elpi Accumulate File util.
 Elpi Accumulate Db trocq.db.
@@ -152,7 +151,6 @@ Elpi Accumulate lp:{{
     FinalProof = {{ @comap lp:G lp:G' lp:GR (_ : lp:G') }},
     util.when-debug dbg.full (coq.say FinalProof),
 
-    % TODO: explain why we need elaboration + typechecking + unification
     std.assert-ok! (coq.elaborate-skeleton FinalProof G EFinalProof) "proof elaboration error",
     std.assert-ok! (coq.typecheck EFinalProof G2) "proof typechecking error",
     std.assert-ok! (coq.unify-leq G2 G) "goal unification error",