diff --git a/THANKS b/THANKS
index 784b6b337..298397ead 100644
--- a/THANKS
+++ b/THANKS
@@ -33,6 +33,7 @@ Michael Weber
 Mikuláš Klokočka
 Ming-Hsien Tsai
 Nikos Gorogiannis
+Paul Guénézan
 Reuben Rowe
 Rüdiger Ehlers
 Silien Hong
diff --git a/doc/org/concepts.org b/doc/org/concepts.org
index 7df9f5880..6fe52c5bb 100644
--- a/doc/org/concepts.org
+++ b/doc/org/concepts.org
@@ -21,7 +21,7 @@ true if the light is on and the door open, and false otherwise.
 
 Atomic propositions are used to construct temporal logic formulas (see
 below) to specify properties of the system: for instance we might want
-to state that /whenever the the door is open, the light should be on/.
+to state that /whenever the door is open, the light should be on/.
 We could write that as the [[#ltl][LTL formula]] =G(door_open -> light_on)= in
 which =G= is a temporal operator that means /always/.