diff --git a/THANKS b/THANKS
index 7d3596140..cd1a8be60 100644
--- a/THANKS
+++ b/THANKS
@@ -33,6 +33,7 @@ Kristin Y. Rozier
 Martin Dieguez Lodeiro
 Matthias Heizmann
 Maxime Bouton
+Michaël Cadilhac
 Michael Tautschnig
 Michael Weber
 Mikuláš Klokočka
diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh
index bcd7045f0..507bc849e 100644
--- a/spot/graph/graph.hh
+++ b/spot/graph/graph.hh
@@ -1289,10 +1289,19 @@ namespace spot
 
     /// \brief Rename and remove states.
     ///
-    /// \param newst A vector indicating how each state should be renumbered.
-    /// Use -1U to erase a state.  All other numbers are expected to
-    /// satisfy newst[i] ≤ i for all i.
-    /// \param used_states the number of states used (after renumbering)
+    /// This method is used to remove some states that have been
+    /// previously detected to be unreachable in order to "defragment"
+    /// the state vector.  When a state is removed, all its outgoing
+    /// transition are removed as well.  Removing reachable states
+    /// should NOT be attempted, because the incoming edges will be
+    /// dangling.
+    ///
+    /// \param newst A vector indicating how each state should be
+    /// renumbered.  Use -1U to erase an unreachable state.  All other
+    /// numbers are expected to satisfy newst[i] ≤ i for all i.
+    ///
+    /// \param used_states the number of states used (after
+    /// renumbering)
     void defrag_states(std::vector<unsigned>&& newst, unsigned used_states)
     {
       SPOT_ASSERT(newst.size() >= states_.size());
diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh
index 2f49d7b16..b8e248916 100644
--- a/spot/twa/twagraph.hh
+++ b/spot/twa/twagraph.hh
@@ -559,7 +559,7 @@ namespace spot
     ///
     /// In the second pass, edges that share their source, destination,
     /// and acceptance marks are merged into a single edge whose condition
-    /// is the conjunction of the conditions of the original edges.
+    /// is the disjunction of the conditions of the original edges.
     ///
     /// If the automaton uses some universal edges, the method
     /// merge_univ_dests() is also called.
@@ -695,12 +695,20 @@ namespace spot
     /// digraph::defrag_state() that additionally deals with universal
     /// branching.
     ///
+    /// This method is used to remove some states that have been
+    /// previously detected to be unreachable in order to "defragment"
+    /// the state vector.  When a state is removed, all its outgoing
+    /// transition are removed as well.  Removing reachable states
+    /// should NOT be attempted, because the incoming edges will be
+    /// dangling.
+    ///
     /// \param newst A vector indicating how each state should be
-    /// renumbered.  Use -1U to erase a state.  Ignoring the
-    /// occurrences of -1U, the renumbering is expected to
-    /// satisfy newst[i] ≤ i for all i.
-    /// \param used_states the number of states used
-    /// (after renumbering)
+    /// renumbered.  Use -1U to mark an unreachable state for removal.
+    /// Ignoring the occurrences of -1U, the renumbering is expected
+    /// to satisfy newst[i] ≤ i for all i.
+    ///
+    /// \param used_states the number of states used after
+    /// renumbering.
     void defrag_states(std::vector<unsigned>&& newst, unsigned used_states);
 
     /// \brief Print the data structures used to represent the