diff options
author | 2015-06-23 10:12:41 +0200 | |
---|---|---|
committer | 2016-06-05 22:09:39 -0400 | |
commit | 9ff2c9d8d042c9989b6a8138c308398c49ae116f (patch) | |
tree | ab6abf0403a4db27fef257393795111284da20ae /test-suite/success | |
parent | 45748e4efae8630cc13b0199dfcc9803341e8cd8 (diff) |
LtacProf for Coq trunk
This add LtacProfiling. Much of the code was written by Tobias Tebbi
(@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq
v8.5 and Coq trunk.
Diffstat (limited to 'test-suite/success')
-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..6b73443d6 --- /dev/null +++ b/test-suite/success/ltacprof.v @@ -0,0 +1,8 @@ +(** Some LtacProf tests *) + +Start Profiling. +Ltac multi := (idtac + idtac). +Goal True. + try (multi; fail). (* Anomaly: Uncaught exception Failure("hd"). Please report. *) +Admitted. +Show Profile. |