diff options
| author | Jason Gross | 2016-05-15 16:05:11 -0400 |
|---|---|---|
| committer | Jason Gross | 2016-06-05 22:09:41 -0400 |
| commit | 9b0376731de3b71a7461747d12763becca1e5399 (patch) | |
| tree | 4eeaff5d0238034a7232e8b5778419dcd85444aa /test-suite | |
| parent | 13e11b6aec1444071dc3787da15e89a6bc0eb0dc (diff) | |
Make Ltac Profiling an setting
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/ltacprof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v index 6b73443d6a..ae11358eda 100644 --- a/test-suite/success/ltacprof.v +++ b/test-suite/success/ltacprof.v @@ -1,8 +1,8 @@ (** Some LtacProf tests *) -Start Profiling. +Set Ltac Profiling. Ltac multi := (idtac + idtac). Goal True. try (multi; fail). (* Anomaly: Uncaught exception Failure("hd"). Please report. *) Admitted. -Show Profile. +Show Ltac Profile. |