diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/ltacprof.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v new file mode 100644 index 000000000..d5552695c --- /dev/null +++ b/test-suite/success/ltacprof.v @@ -0,0 +1,8 @@ +(** Some LtacProf tests *) + +Set Ltac Profiling. +Ltac multi := (idtac + idtac). +Goal True. + try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *) +Admitted. +Show Ltac Profile. |