diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index c465ec0a6aa1e7537335b355b99c9316e201fa02..69816014649b025cb7b81cc09e7e45c9517df24e 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -246,8 +246,16 @@ and nodeStatus =
   | Sat
   | Unsat
 
+(* In K, given the singleton list [bs] returns the list of all Ax'es
+   responsible for the individual members of bs being part of the core
+   as well as the Ex.
+
+   So given the state { <>φ , []ψ , []η } and the core { φ , ψ , η },
+   dependency would map { η } to { <>φ , []η } and { ψ } to { <>φ , []ψ }
+*)
 and dependencies = bset list -> bset
 
+(* Note: sort * bset * bset is to be read as sort * formulas_in_core * deferrals_in_core *)
 and rule = (dependencies * (sort * bset * bset) lazylist)
 
 and 'a lazyliststep =