diff options
| author | narboux | 2003-11-12 18:03:50 +0000 |
|---|---|---|
| committer | narboux | 2003-11-12 18:03:50 +0000 |
| commit | ecf5fbd6bc5fc12166dd36c1b12ec714b86d0a63 (patch) | |
| tree | 2c9927b2d22c456dd07daddff5cc56cabdfb8b2d /proofs | |
| parent | ea9f6b8f620b9f69de9d72ca603af042e4487339 (diff) | |
Idtac peut prendre un argument à afficher
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4863 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |