diff --git a/doc/todo.md b/doc/todo.md
index 14c234f25..bb2f2db22 100644
--- a/doc/todo.md
+++ b/doc/todo.md
@@ -15,3 +15,4 @@ To Do List
 - Independent type checker using a different programming language (e.g., F* or OCaml).
 - Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs.
 - Re-implement apply-tactic.
+- Improve performance of `is_convertible` and `is_definitionally_equal` predicates