From 6b78930640a03260f98fa90411070c6dbad8d266 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 20 May 2016 13:45:08 -0400
Subject: Improve a comment in the test suite

---
 test-suite/success/ltacprof.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v
index ae11358eda..d5552695c4 100644
--- a/test-suite/success/ltacprof.v
+++ b/test-suite/success/ltacprof.v
@@ -3,6 +3,6 @@
 Set Ltac Profiling.
 Ltac multi := (idtac + idtac).
 Goal True.
-  try (multi; fail). (* Anomaly: Uncaught exception Failure("hd"). Please report. *)
+  try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *)
 Admitted.
 Show Ltac Profile.
-- 
cgit v1.2.3