From ff007045f1a393caa01fbe14bb44f528ce906940 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 15 Dec 2018 11:24:29 +0100
Subject: [PATCH] Improve a comment.

---
 theories/proofmode/ltac_tactics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 2f7c2742e..bccbbcf85 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) :=
-- 
GitLab