diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 2f7c2742e6be741124d66397b0279a808b90fc52..bccbbcf852f231ef8622b878e92c25d7621b0234 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -127,8 +127,8 @@ pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:
 
   https://sympa.inria.fr/sympa/arc/coq-club/2018-01/msg00000.html
 
-PMP told me (= Robbert) in person that this is not possible today, but may be
-possible in Ltac2. *)
+PMP told me (= Robbert) in person that this is not possible with the current
+Ltac, but it may be possible in Ltac2. *)
 
 (** * Context manipulation *)
 Tactic Notation "iRename" constr(H1) "into" constr(H2) :=