aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Rename.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/Rename.v')
-rw-r--r--test-suite/success/Rename.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/Rename.v b/test-suite/success/Rename.v
index 0576f3c68..2789c6c9a 100644
--- a/test-suite/success/Rename.v
+++ b/test-suite/success/Rename.v
@@ -4,7 +4,7 @@ rename n into p.
induction p; auto.
Qed.
-(* Submitted by Iris Loeb (#842) *)
+(* Submitted by Iris Loeb (BZ#842) *)
Section rename.