diff options
| author | Hugo Herbelin | 2014-07-03 12:43:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-07-07 21:30:18 +0200 |
| commit | abad0a15ac44cb5b53b87382bb4d587d9800a0f6 (patch) | |
| tree | accb7680bdff39d8e9233f30c0fe8990eddac2a6 /tactics/tacinterp.ml | |
| parent | 8e767acc26cb2335f1a8dac3c4c184e2cc0b64c4 (diff) | |
time tac
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c749e2d720..b70f214316 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1023,6 +1023,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacThens (t1,tl) -> Tacticals.New.tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl) | TacDo (n,tac) -> Tacticals.New.tclDO (interp_int_or_var ist n) (interp_tactic ist tac) | TacTimeout (n,tac) -> Tacticals.New.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac) + | TacTime tac -> Tacticals.New.tclTIME (interp_tactic ist tac) | TacTry tac -> Tacticals.New.tclTRY (interp_tactic ist tac) | TacRepeat tac -> Tacticals.New.tclREPEAT (interp_tactic ist tac) | TacOr (tac1,tac2) -> |