diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 10 | ||||
| -rw-r--r-- | proofs/refiner.mli | 6 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 2 |
3 files changed, 14 insertions, 4 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 601359590a..489c3f5c0b 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -342,9 +342,17 @@ let idtac_valid = function (* [goal_goal_list : goal sigma -> goal list sigma] *) let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma} -(* the identity tactic *) +(* identity tactic without any message *) let tclIDTAC gls = (goal_goal_list gls, idtac_valid) +(* the message printing identity tactic *) +let tclIDTAC_MESSAGE s gls = + if s = "" then tclIDTAC gls + else + begin + msgnl (str ("Idtac says : "^s)); tclIDTAC gls + end + (* General failure tactic *) let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 0107a3943a..9b45ad4f91 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -64,8 +64,10 @@ val frontier_mapi : (*s Tacticals. *) -(* [tclIDTAC] is the identity tactic *) -val tclIDTAC : tactic +(* [tclIDTAC] is the identity tactic without message printing*) +val tclIDTAC : tactic +val tclIDTAC_MESSAGE : string -> tactic + (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 5de120dbbb..f1c5763289 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -194,7 +194,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr = | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * identifier option - | TacId + | TacId of string | TacFail of int * string | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr |