diff --git a/THANKS b/THANKS
index 54fa34fa7..6cca9ada1 100644
--- a/THANKS
+++ b/THANKS
@@ -15,5 +15,6 @@ Michael Weber
 Nikos Gorogiannis
 Rüdiger Ehlers
 Silien Hong
+Sonali Dutta
 Tomáš Babiak
 Yann Thierry-Mieg
diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh
index 1cc4c0f21..4198ab45c 100644
--- a/src/tgba/bdddict.hh
+++ b/src/tgba/bdddict.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
+// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -44,11 +44,25 @@ namespace spot
   /// atomic propositions, but they can also be acceptance conditions,
   /// or "Now/Next" variables (although the latter should be
   /// eventually removed).
+  ///
+  /// When a BDD variable is registered using a bdd_dict, it is always
+  /// associated to a "user" (or "owner") object.  This is done by
+  /// supplying the bdd_dict with a pointer to the intended user of
+  /// the variable.  When the user object dies, it should release the
+  /// BDD variables it was using by calling (for instance)
+  /// unregister_all_my_variables(), giving the same pointer.
+  /// Variables can also by unregistered one by one using
+  /// unregister_variable().
   class bdd_dict: public bdd_allocator
   {
   public:
 
     bdd_dict();
+
+    /// \brief Destroy the BDD dict.
+    ///
+    /// This always calls assert_emptiness() to diagnose cases where
+    /// variables have not been unregistered.
     ~bdd_dict();
 
     /// Formula-to-BDD-variable maps.
@@ -206,8 +220,15 @@ namespace spot
 
     /// \brief Make sure the dictionary is empty.
     ///
-    /// This will print diagnostics and abort if the dictionary
-    /// is not empty.  Use for debugging.
+    /// This will print diagnostics if the dictionary is not empty.
+    /// Use for debugging.  This is called automatically by the
+    /// destructor.  When Spot is compiled in development mode (i.e.,
+    /// with <code>./configure --enable-devel</code>), this function
+    /// will abort if the dictionary is not empty.
+    ///
+    /// The errors detected by this function usually indicate missing
+    /// calls to unregister_variable() or
+    /// unregister_all_my_variables().
     void assert_emptiness() const;
 
   protected:
diff --git a/src/tgba/formula2bdd.hh b/src/tgba/formula2bdd.hh
index 4c98c26db..b3d746e05 100644
--- a/src/tgba/formula2bdd.hh
+++ b/src/tgba/formula2bdd.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Développement de
+// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 // Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -28,14 +28,27 @@
 
 namespace spot
 {
-  /// \brief Convert a formula into a BDD.
+  /// \brief Convert a Boolean formula into a BDD.
   ///
-  /// Convert formula \a f into a Bdd, using existing variables from \a
-  /// d, and registering new one as necessary.  \a for_me is the
-  /// address to use as owner of the variables used in the BDD.
+  /// Convert the Boolean formula \a f into a BDD, using existing
+  /// variables from \a d, and registering new ones as necessary.  \a
+  /// for_me, the address of the user of these BDD variables will be
+  /// passed to \a d when registering the variables.
+  ///
+  /// If you only use the BDD representation temporarily, for instance
+  /// passing it right away to bdd_to_formula(), you should not forget
+  /// to unregister the variables that have been registered for \a
+  /// for_me.  See bdd_dict::unregister_all_my_variables().
   bdd formula_to_bdd(const ltl::formula* f, bdd_dict* d, void* for_me);
 
-  /// Convert a BDD into a formula.
+  /// \brief Convert a BDD into a formula.
+  ///
+  /// Format the BDD as an irredundant sum of product (see the
+  /// minato_isop class for details) and map the BDD variables back
+  /// into their atomic propositions.  This works only for Boolean
+  /// formulas, and all the BDD variables used in \a f should have
+  /// been registered in \a d.  Although the result has type
+  /// ltl::formula*, it obviously does not use any temporal operator.
   const ltl::formula* bdd_to_formula(bdd f, const bdd_dict* d);
 }