diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 30c882618760e930b14a9d268312cdf200401e95..c61a243aa86893233761a7d77a7d2a752355c04e 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -35,13 +35,13 @@ definitions being unfolded (see issue #55).
 For binary connectives we have the following instances:
 
 <<
-ProgIntoLaterN n P P'       IntoLaterN n Q Q'
----------------------------------------------
-ProgIntoLaterN n (P /\ Q) (P' /\ Q')
+IntoLaterN' n P P'       IntoLaterN n Q Q'
+------------------------------------------
+     IntoLaterN' n (P /\ Q) (P' /\ Q')
 
 
-   ProgIntoLaterN n Q Q'
---------------------------------
+      IntoLaterN' n Q Q'
+-------------------------------
 IntoLaterN n (P /\ Q) (P /\ Q')
 >>
 *)