Idtac peut prendre un argument à afficher

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

6 files changed, 11 insertions, 10 deletions

diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index fc20b9c76e..a124cf5df8 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 152b80e2a3..18b8f7326f 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 56a5f6e46a..cfcbe9a917 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 09964a3311..52a12a23d8 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 943577e1b4..7ff64996b3 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 001e762d11..54f265c85b 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)