diff options
| author | Jason Gross | 2016-05-20 13:45:08 -0400 |
|---|---|---|
| committer | Jason Gross | 2016-06-05 22:09:41 -0400 |
| commit | 6b78930640a03260f98fa90411070c6dbad8d266 (patch) | |
| tree | 7942c85808f684630b96ee8f01a1eac7327493d5 | |
| parent | 9b0376731de3b71a7461747d12763becca1e5399 (diff) | |
Improve a comment in the test suite
| -rw-r--r-- | test-suite/success/ltacprof.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |