diff --git a/THANKS b/THANKS
index 856eac58b..e73f40175 100644
--- a/THANKS
+++ b/THANKS
@@ -1,7 +1,9 @@
 We are grateful to these people for their comments, help, or
 suggestions.
 
+Christian Dax
 Étienne Renault
+Felix Klaedtke
 Gerard J. Holzmann
 Heikki Tauriainen
 Jean-Michel Couvreur
diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index fc51ff2b5..a61f72547 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -1427,6 +1427,10 @@ namespace spot
 	      // Transitions going to destinations accepting the empty
 	      // word should recognize f2, and the automaton for f1
 	      // should be understood as universal.
+	      //
+	      // The crux of this translation (the use of implication,
+	      // and the interpretation as a universal automaton) was
+	      // explained to me (adl) by Felix Klaedtke.
 	      bdd f2 = recurse(node->second());
 	      bdd f1 = translate_ratexp(node->first(), dict_);
 	      res_ = bddtrue;