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 | |
| parent | 8e767acc26cb2335f1a8dac3c4c184e2cc0b64c4 (diff) | |
time tac
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 1 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 1 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 3 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 |
5 files changed, 8 insertions, 0 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index f68f753599..033e004336 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -613,6 +613,8 @@ and intern_tactic_seq onlytac ist = function | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac) | TacTimeout (n,tac) -> ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic onlytac ist tac) + | TacTime tac -> + ist.ltacvars, TacTime (intern_tactic onlytac ist tac) | TacOr (tac1,tac2) -> ist.ltacvars, TacOr (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) | TacOnce tac -> 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) -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 4dd4b0aa81..8ab63c1610 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -230,6 +230,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl) | TacDo (n,tac) -> TacDo (n,subst_tactic subst tac) | TacTimeout (n,tac) -> TacTimeout (n,subst_tactic subst tac) + | TacTime tac -> TacTime (subst_tactic subst tac) | TacTry tac -> TacTry (subst_tactic subst tac) | TacInfo tac -> TacInfo (subst_tactic subst tac) | TacRepeat tac -> TacRepeat (subst_tactic subst tac) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index fcce6e5eba..267a34754e 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -467,6 +467,9 @@ module New = struct | e -> Proofview.tclZERO e end + let tclTIME t = + Proofview.tclTIME t + let nthDecl m gl = let hyps = Proofview.Goal.hyps gl in try diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 48fd44b4ab..705a7e2cce 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -212,6 +212,7 @@ module New : sig val tclWITHHOLES : bool -> ('a -> unit tactic) -> Evd.evar_map -> 'a -> unit tactic val tclTIMEOUT : int -> unit tactic -> unit tactic + val tclTIME : 'a tactic -> 'a tactic val nLastDecls : [ `NF ] Proofview.Goal.t -> int -> named_context |