Idtac peut prendre un argument à afficher

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4863 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 1 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)