diff options
| author | courtieu | 2012-10-01 16:17:51 +0000 |
|---|---|---|
| committer | courtieu | 2012-10-01 16:17:51 +0000 |
| commit | d3b2c6f8a6864c44236b1f4b2ac89a025f49b7cd (patch) | |
| tree | 94985eacc1c3b416b9707802a4d2d2f8a5e8d5f9 /tactics | |
| parent | 4a10b5e505df255a7ff8efa68214a14f50c24576 (diff) | |
Added a new tactical infoH tac, that displays the names of hypothesis created by tac, in the 'as' format. Interfaces can use this to insert automatically an 'as' close at the end of the tactic (afterward).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15839 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |