diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 4 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 1 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 |
3 files changed, 5 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 057a268f56..9bbb095893 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -839,7 +839,7 @@ and intern_tactic_seq onlytac ist = function | TacId l -> ist.ltacvars, TacId (intern_message ist l) | TacFail (n,l) -> ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l) - | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac) + | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac) | TacShowHyps tac -> ist.ltacvars, TacShowHyps (intern_pure_tactic ist tac) | TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_pure_tactic ist tac,s) | TacThen (t1,[||],t2,[||]) -> @@ -1809,6 +1809,7 @@ and eval_tactic ist = function db_breakpoint ist.debug s; res | TacFail (n,s) -> fun gl -> tclFAIL (interp_int_or_var ist n) (interp_message ist gl s) gl | TacProgress tac -> tclPROGRESS (interp_tactic ist tac) + | TacShowHyps tac -> tclSHOWHYPS (interp_tactic ist tac) | TacAbstract (tac,ido) -> fun gl -> Tactics.tclABSTRACT (Option.map (pf_interp_ident ist gl) ido) (interp_tactic ist tac) gl @@ -2940,6 +2941,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with TacMatch (lz,subst_tactic subst c,subst_match_rule subst lmr) | TacId _ | TacFail _ as x -> x | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr) + | TacShowHyps tac -> TacShowHyps (subst_tactic subst tac:glob_tactic_expr) | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s) | TacThen (t1,tf,t2,tl) -> TacThen (subst_tactic subst t1,Array.map (subst_tactic subst) tf, diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 637269a663..69cee21487 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -53,6 +53,7 @@ let tclDO = Refiner.tclDO let tclTIMEOUT = Refiner.tclTIMEOUT let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS let tclPROGRESS = Refiner.tclPROGRESS +let tclSHOWHYPS = Refiner.tclSHOWHYPS let tclNOTSAMEGOAL = Refiner.tclNOTSAMEGOAL let tclTHENTRY = Refiner.tclTHENTRY let tclIFTHENELSE = Refiner.tclIFTHENELSE diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 4e9198d37d..39f60e1968 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -54,6 +54,7 @@ val tclFAIL_lazy : int -> std_ppcmds Lazy.t -> tactic val tclDO : int -> tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic val tclPROGRESS : tactic -> tactic +val tclSHOWHYPS : tactic -> tactic val tclNOTSAMEGOAL : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclMAP : ('a -> tactic) -> 'a list -> tactic |