diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-07 21:34:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-07 21:34:49 +0200 |
| commit | a3503c0aca07f5e7f5785faa7b76123a02ecc2af (patch) | |
| tree | ae07277425e50314b0c341752a11af3055a01907 /tactics | |
| parent | abad0a15ac44cb5b53b87382bb4d587d9800a0f6 (diff) | |
Revert "time tac" (committed by mistake).
This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
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, 0 insertions, 8 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 033e00433..f68f75359 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -613,8 +613,6 @@ 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 b70f21431..c749e2d72 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1023,7 +1023,6 @@ 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 8ab63c161..4dd4b0aa8 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -230,7 +230,6 @@ 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 267a34754..fcce6e5eb 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -467,9 +467,6 @@ 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 705a7e2cc..48fd44b4a 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -212,7 +212,6 @@ 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 |