Idtac peut prendre un argument à afficher

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

17 files changed, 37 insertions, 24 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 41ee54ea4..51480a956 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -166,7 +166,7 @@ GEXTEND Gram
 	  TacFirst l
       | IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
 	  TacSolve l
-      | IDENT "Idtac" -> TacId
+      | IDENT "Idtac" ; s = [ s = STRING -> s | -> ""] -> TacId s
       | IDENT "Fail"; n = [ n = natural -> n | -> fail_default_value ];
 	  s = [ s = STRING -> s | -> ""] -> TacFail (n,s)
       | st = simple_tactic -> TacAtom (loc,st)
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index aaf31da53..1f0241526 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -110,7 +110,7 @@ GEXTEND Gram
 	  TacFirst l
       | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
 	  TacSolve l
-      | IDENT "idtac" -> TacId
+      | IDENT "idtac"; s = [ s = STRING -> s | -> ""] -> TacId s		
       | IDENT "fail"; n = [ n = natural -> n | -> fail_default_value ];
 	  s = [ s = STRING -> s | -> ""] -> TacFail (n,s)
       | st = simple_tactic -> TacAtom (loc,st)
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index c462c3bdc..638591460 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -36,7 +36,7 @@ GEXTEND Gram
   ;
   command:
     [ [ IDENT "Goal"; c = Constr.constr -> VernacGoal c
-      | "Proof" -> VernacProof Tacexpr.TacId
+      | "Proof" -> VernacProof (Tacexpr.TacId "")
       | "Proof"; "with"; ta = tactic -> VernacProof ta
       | IDENT "Abort" -> VernacAbort None
       | IDENT "Abort"; IDENT "All" -> VernacAbortAll
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index ea5ad236e..4397f6769 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -565,7 +565,7 @@ and pr_tactic_seq_body tl =
 and pr0 = function
   | TacFirst tl -> str "First" ++ spc () ++ pr_tactic_seq_body tl
   | TacSolve tl -> str "Solve" ++ spc () ++ pr_tactic_seq_body tl
-  | TacId -> str "Idtac"
+  | TacId "" -> str "Idtac" 
   | TacFail (0,"") -> str "Fail"
   | TacAtom (_,t) -> pr_atom0 t
   | TacArg c -> pr_tacarg c
@@ -574,6 +574,7 @@ and pr0 = function
   (* Semi-closed atomic tactic expressions *)
 and pr1 = function
   | TacAtom (_,t) -> pr_atom1 t
+  | TacId s -> str "Idtac \"" ++ str s ++ str "\""	
   | TacFail (0,s) -> str "Fail \"" ++ str s ++ str "\""
   | TacFail (n,"") -> str "Fail " ++ int n
   | TacFail (n,s) -> str "Fail " ++ int n ++ str " \"" ++ str s ++ str "\""
@@ -619,7 +620,7 @@ and pr6 = function
   | TacDo _
   | TacRepeat _
   | TacProgress _
-  | TacId
+  | TacId _
   | TacFail _
   | TacInfo _) as t -> pr5 t
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 01be09fc6..dfe341beb 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -470,7 +470,7 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
       <:expr< Tacexpr.TacRepeat $mlexpr_of_tactic t$ >>
   | Tacexpr.TacProgress t ->
       <:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacId -> <:expr< Tacexpr.TacId >>
+  | Tacexpr.TacId s -> <:expr< Tacexpr.TacId $str:s$ >>
   | Tacexpr.TacFail (n,s) -> <:expr< Tacexpr.TacFail $int:string_of_int n$ $str:s$ >>
 (*
   | Tacexpr.TacInfo t -> TacInfo (loc,f t)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 601359590..489c3f5c0 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 0107a3943..9b45ad4f9 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 5de120dbb..f1c576328 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
 
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index fc20b9c76..a124cf5df 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -293,7 +293,7 @@ let applyDestructor cls discard dd gls =
       | (Some id,HypLocation(discardable,_,_)) ->
           if discard & discardable then thin [id] else tclIDTAC
       | (None,ConclLocation _) -> tclIDTAC
-      | _ -> error "ApplyDestructor" 
+       | _ -> error "ApplyDestructor" 
   in
   tclTHEN (!forward_interp_tactic tac) discard_0 gls
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 152b80e2a..18b8f7326 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -134,7 +134,7 @@ let add_rewrite_hint name ort t lcsr =
 (* V7 *)
 VERNAC COMMAND EXTEND HintRewriteV7
   [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b) ] ->
-  [ add_rewrite_hint b o Tacexpr.TacId l ]
+  [ add_rewrite_hint b o (Tacexpr.TacId "") l ]
 | [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b)
     "using" tactic(t) ] ->
   [ add_rewrite_hint b o t l ]
@@ -143,7 +143,7 @@ END
 (* V8 *)
 VERNAC COMMAND EXTEND HintRewriteV8
   [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident(b) ] ->
-  [ add_rewrite_hint b o Tacexpr.TacId l ]
+  [ add_rewrite_hint b o (Tacexpr.TacId "") l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
     ":" preident(b) ] ->
   [ add_rewrite_hint b o t l ]
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 56a5f6e46..cfcbe9a91 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -678,7 +678,7 @@ and intern_tactic_seq ist = function
   (* Traducteur v7->v8 *)
   | TacAtom (_,TacReduce (Unfold [_,Ident (_,id)],_))
       when string_of_id id = "INZ" & !Options.translate_syntax
-        -> ist.ltacvars, TacId
+        -> ist.ltacvars, (TacId "")
   (* Fin traducteur v7->v8 *)
 
   | TacAtom (loc,t) ->
@@ -703,8 +703,7 @@ and intern_tactic_seq ist = function
       ist.ltacvars, TacMatchContext(lr, intern_match_rule ist lmr)
   | TacMatch (c,lmr) ->
       ist.ltacvars, TacMatch (intern_tactic ist c,intern_match_rule ist lmr)
-  | TacId -> ist.ltacvars, TacId
-  | TacFail _ as x -> ist.ltacvars, x
+  | TacId _ | TacFail _ as x -> ist.ltacvars, x
   | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
   | TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s)
   | TacThen (t1,t2) ->
@@ -1239,7 +1238,7 @@ and eval_tactic ist = function
   | TacLetIn (l,u) -> assert false
   | TacMatchContext _ -> assert false
   | TacMatch (c,lmr) -> assert false
-  | TacId -> tclIDTAC
+  | TacId s -> tclIDTAC_MESSAGE s
   | TacFail (n,s) -> tclFAIL n s
   | TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
   | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (interp_tactic ist tac)
@@ -1915,7 +1914,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
       TacMatchContext(lr, subst_match_rule subst lmr)
   | TacMatch (c,lmr) ->
       TacMatch (subst_tactic subst c,subst_match_rule subst lmr)
-  | TacId | TacFail _ as x -> x
+  | TacId _ | TacFail _ as x -> x
   | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
   | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
   | TacThen (t1,t2) ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 09964a331..52a12a23d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -36,6 +36,7 @@ open Tacexpr
 (*************************************************)
 
 let tclIDTAC         = tclIDTAC
+let tclIDTAC_MESSAGE = tclIDTAC_MESSAGE
 let tclORELSE        = tclORELSE
 let tclTHEN          = tclTHEN
 let tclTHENLIST      = tclTHENLIST
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 943577e1b..7ff64996b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -23,6 +23,7 @@ open Tacexpr
 (* Tacticals i.e. functions from tactics to tactics. *)
 
 val tclIDTAC         : tactic
+val tclIDTAC_MESSAGE : string -> tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclTHEN          : tactic -> tactic -> tactic
 val tclTHENSEQ       : tactic list -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 001e762d1..54f265c85 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -297,7 +297,7 @@ let central_intro = intro_gen
 
 let rec intros_using = function
     []      -> tclIDTAC
-  | str::l  -> tclTHEN (intro_using str) (intros_using l)
+   | str::l  -> tclTHEN (intro_using str) (intros_using l)
 
 let intros = tclREPEAT (intro_force false)
 
@@ -538,7 +538,7 @@ let cut_replacing id t =
 
 let cut_in_parallel l = 
   let rec prec = function
-    | [] -> tclIDTAC
+    | [] -> tclIDTAC 
     | h::t -> tclTHENFIRST (cut h) (prec t)
   in 
   prec (List.rev l)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 541422261..5edc4eaf8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -580,8 +580,8 @@ let vernac_solve_existential = instantiate_nth_evar_com
 let vernac_set_end_tac tac =
   if not (refining ()) then
     error "Unknown command of the non proof-editing mode";
-  if tac <> Tacexpr.TacId then set_end_tac (Tacinterp.interp tac)
-
+  if tac <> (Tacexpr.TacId "") then set_end_tac (Tacinterp.interp tac)
+(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
  
    
 (*****************************)
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 7b9ba49d8..a0ef088f7 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -678,7 +678,8 @@ let rec pr_tac env inherited tac =
       str "first" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
   | TacSolve tl ->
       str "solve" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
-  | TacId -> str "idtac", latom
+  | TacId "" -> str "idtac", latom
+  | TacId s -> str "idtac" ++ (qsnew s), latom
   | TacAtom (loc,t) ->
       pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom
   | TacArg(Tacexp e) -> pr_tac0 env e, latom
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 2a8cc3c9b..c7602c2b0 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -1040,7 +1040,7 @@ let rec pr_vernac = function
   | VernacExtend (s,c) -> pr_extend s c
   | VernacV7only _ -> mt()
   | VernacV8only com -> pr_vernac com
-  | VernacProof Tacexpr.TacId -> str "Proof"
+  | VernacProof Tacexpr.TacId _ -> str "Proof"
   | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te 
 
 and pr_extend s cl =