diff options
| -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. |