Bug TacId

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

4 files changed, 8 insertions, 7 deletions

diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index ca43d00778..bf596b2842 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -355,7 +355,7 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
 	  Report_node(true, n, l) -> tac
       	| Report_node(false, n, rl) ->
 	    TacThens (a,List.map2 reconstruct_success_tac l rl)
-      	| Failed n -> TacId
+      	| Failed n -> TacId ""
       	| Tree_fail r -> reconstruct_success_tac a r
       	| Mismatch (n,p) -> a)
   | TacThen (a,b) ->
@@ -367,13 +367,13 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
 	      [in_gen globwit_tactic a;
 	       in_gen globwit_tactic b;
 	       in_gen (wit_list0 globwit_int) selected_indices]))
-	| Failed n -> TacId
+	| Failed n -> TacId ""
 	| Tree_fail r -> reconstruct_success_tac a r
 	| _ -> error "this error case should not happen in a THEN tactic")
   | _ -> 
       (function
 	  Report_node(true, n, l) -> tac
-	| Failed n -> TacId
+	| Failed n -> TacId ""
 	| _ ->
 	    errorlabstrm
 	      "this error case should not happen on an unknown tactic"
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index f8f242a446..eb7c6a2059 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -154,7 +154,7 @@ let make_pbp_pattern x =
      [make_var (id_of_string ("Value_for_" ^ (string_of_id x)))]
 
 let rec make_then = function
-  | [] -> TacId
+  | [] -> TacId ""
   | [t] -> t
   | t1::t2::l -> make_then (TacThen (t1,t2)::l)
 
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index f2f56caa87..ecc9d1babc 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1263,7 +1263,7 @@ let rec natural_ntree ig ntree =
                                   tag_toprove g  ]
 			  ]
 
-      | Proof (TacId,ltree) -> natural_ntree ig (List.hd ltree)
+      | Proof (TacId _,ltree) -> natural_ntree ig (List.hd ltree)
       | Proof (TacAtom (_,tac),ltree) -> 
 	 (let ntext = 
 	  match tac with
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 3f3c3ba615..41de42b725 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -772,7 +772,8 @@ and xlate_tactic =
    | TacAtom (_, t) -> xlate_tac t 
    | TacFail (n,"") -> CT_fail (CT_int n)
    | TacFail (n,s) -> xlate_error "TODO: Fail n message"
-   | TacId -> CT_idtac
+   | TacId "" -> CT_idtac
+   | TacId _ -> xlate_error "TODO: Idtac with argument"
    | TacInfo t -> CT_info(xlate_tactic t)
    | TacArg a -> xlate_call_or_tacarg a
 
@@ -1353,7 +1354,7 @@ let xlate_vernac =
       let formula_list = out_gen (wit_list1 (rawwit_constr)) formula_list in
       let base = out_gen rawwit_pre_ident base in
       let t = match t with
-	| [] -> TacId
+	| [] -> TacId ""
 	| [t] -> out_gen rawwit_tactic t
 	| _ -> failwith "" in
       let ct_orient = match orient with