Globalisation des noms de tactiques dans les définitions de tactiques

pour compatibilité avec les modules.
Globalisation partielle des invocations de tactiques hors définitions
(partielle car noms des Intros/Assert/Inversion/... non connus).


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

7 files changed, 32 insertions, 32 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index ce43da5ded..7d3ed8dd83 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -583,7 +583,7 @@ let blast gls =
     (* on remplace les ?1 ?2 ... de refine par ? *)
 		parse_tac ((vire_extvar tac_string)
 			   ^ ".")
-		)
+	  )
 	  else (msgnl (hov 0 (str"Blast failed to prove the goal..."));
 		failwith "echec de blast"))
      with _ -> failwith "echec de blast"
@@ -598,7 +598,8 @@ let blast_tac display_function = function
           |  _ -> failwith "expecting other arguments";;
 
 let blast_tac_txt = 
-  blast_tac (function x -> msgnl(Pptactic.pr_raw_tactic x));;
+  blast_tac
+    (function x -> msgnl(Pptactic.pr_glob_tactic (Tacinterp.glob_tactic x)));;
 
 (* Obsolète ?
 overwriting_add_tactic "Blast1" blast_tac_txt;;
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 87f8c8af10..78de2fb022 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -367,7 +367,7 @@ let debug_tac2_pcoq tac =
 	  (errorlabstrm "DEBUG TACTIC"
 	     (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++
 	      fnl () ++ str "the tactic is" ++ fnl () ++
-	      Pptactic.pr_raw_tactic tac);
+	      Pptactic.pr_glob_tactic tac);
 	   result)
 	with
 	  e ->
@@ -901,11 +901,11 @@ END
  </cpa> *)
 
 TACTIC EXTEND CtDebugTac
-| [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq t ]
+| [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
 END
 
 TACTIC EXTEND CtDebugTac2
-| [ "DebugTac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq t ]
+| [ "DebugTac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
 END
 
 
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index 4f03fb06fd..3eb6e7993d 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -10,6 +10,7 @@ open Environ;;
 open Tactics;;
 open Tacticals;;
 open Pattern;;
+open Matching;;
 open Reduction;;
 open Constrextern;;
 open Constrintern;;
diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index 343f90d6e5..ca43d00778 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -115,7 +115,7 @@ let count_subgoals2
        card_holder := Recursive_fail(List.hd !new_report_holder));
     result;;
 
-let rec local_interp : raw_tactic_expr -> report_holder -> tactic = function
+let rec local_interp : glob_tactic_expr -> report_holder -> tactic = function
 (*
     Node(_, "TACTICLIST", [a;Node(_, "TACLIST", l)]) ->
       (fun report_holder -> checked_thens report_holder a l)
@@ -142,7 +142,7 @@ let rec local_interp : raw_tactic_expr -> report_holder -> tactic = function
   | t ->
       (fun report_holder g ->
 	try
-	  let (gls, _) as result = Tacinterp.interp t g in
+	  let (gls, _) as result = Tacinterp.eval_tactic t g in
 	  report_holder := (Report_node(true, List.length (sig_it gls), []))
 			    ::!report_holder;
 	  result
@@ -162,7 +162,7 @@ let rec local_interp : raw_tactic_expr -> report_holder -> tactic = function
    - In case of success of the first tactic, but count mismatch, then
      Mismatch n is added to the report holder. *)
 
-and checked_thens: report_holder -> raw_tactic_expr -> raw_tactic_expr list -> tactic = 
+and checked_thens: report_holder -> glob_tactic_expr -> glob_tactic_expr list -> tactic = 
   (fun report_holder t1 l g ->
     let flag = ref true in
     let traceable_t1 = traceable t1 in
@@ -174,7 +174,7 @@ and checked_thens: report_holder -> raw_tactic_expr -> raw_tactic_expr list -> t
            flag (local_interp t1))
       else
 	(check_subgoals_count card_holder (List.length l)
-           flag (Tacinterp.interp t1)) in
+           flag (Tacinterp.eval_tactic t1)) in
     let (gls, _) as result = 
       tclTHEN_i tac_t1
 	(fun i ->
@@ -185,7 +185,7 @@ and checked_thens: report_holder -> raw_tactic_expr -> raw_tactic_expr list -> t
                  local_interp tac_i new_holder g
               else
 		 try
-		   let (gls,_) as result = Tacinterp.interp tac_i g in
+		   let (gls,_) as result = Tacinterp.eval_tactic tac_i g in
 		   let len = List.length (sig_it gls) in
 				   new_holder :=
 		     (Report_node(true, len, []))::!new_holder;
@@ -217,7 +217,7 @@ and checked_thens: report_holder -> raw_tactic_expr -> raw_tactic_expr list -> t
    reporting information about the success of all tactics in the report
    holder. It never fails. *)
 
-and checked_then: report_holder -> raw_tactic_expr -> raw_tactic_expr -> tactic =
+and checked_then: report_holder -> glob_tactic_expr -> glob_tactic_expr -> tactic =
   (fun report_holder t1 t2 g ->
     let flag = ref true in
     let card_holder = ref Fail in
@@ -225,7 +225,7 @@ and checked_then: report_holder -> raw_tactic_expr -> raw_tactic_expr -> tactic
       if traceable t1 then
 	(count_subgoals2 card_holder flag (local_interp t1))
       else
-	(count_subgoals card_holder flag (Tacinterp.interp t1)) in
+	(count_subgoals card_holder flag (Tacinterp.eval_tactic t1)) in
     let new_tree_holder = ref ([] : report_tree list) in
     let (gls, _) as result =
       tclTHEN tac_t1
@@ -235,7 +235,7 @@ and checked_then: report_holder -> raw_tactic_expr -> raw_tactic_expr -> tactic
 	      local_interp t2 new_tree_holder g
 	    else
 	      try
-		let (gls, _) as result = Tacinterp.interp t2 g in
+		let (gls, _) as result = Tacinterp.eval_tactic t2 g in
 	      	new_tree_holder :=
 		  (Report_node(true, List.length (sig_it gls),[]))::
 		  !new_tree_holder;
@@ -267,10 +267,10 @@ let on_then = function [t1;t2;l] ->
   let t1 = out_gen wit_tactic t1 in
   let t2 = out_gen wit_tactic t2 in
   let l = out_gen (wit_list0 wit_int) l in
-  tclTHEN_i (Tacinterp.interp t1)
+  tclTHEN_i (Tacinterp.eval_tactic t1)
     (fun i ->
       if List.mem (i + 1) l then
-      	(Tacinterp.interp t2)
+      	(Tacinterp.eval_tactic t2)
       else
 	tclIDTAC)
   | _ -> anomaly "bad arguments for on_then";;
@@ -348,7 +348,7 @@ let rec reconstruct_success_tac ast =
               (str "error in reconstruction with " ++ fnl () ++
 	       (gentacpr ast)));;
 *)
-let rec reconstruct_success_tac tac =
+let rec reconstruct_success_tac (tac:glob_tactic_expr) =
   match tac with
     TacThens (a,l) ->
       (function 
@@ -364,9 +364,9 @@ let rec reconstruct_success_tac tac =
 	| Report_node(false, n, rl) ->
 	    let selected_indices = select_success 1 rl in
 	    TacAtom (dummy_loc,TacExtend (dummy_loc,"OnThen",
-	      [in_gen rawwit_tactic a;
-	       in_gen rawwit_tactic b;
-	       in_gen (wit_list0 rawwit_int) selected_indices]))
+	      [in_gen globwit_tactic a;
+	       in_gen globwit_tactic b;
+	       in_gen (wit_list0 globwit_int) selected_indices]))
 	| Failed n -> TacId
 	| Tree_fail r -> reconstruct_success_tac a r
 	| _ -> error "this error case should not happen in a THEN tactic")
@@ -378,7 +378,7 @@ let rec reconstruct_success_tac tac =
 	    errorlabstrm
 	      "this error case should not happen on an unknown tactic"
               (str "error in reconstruction with " ++ fnl () ++
-	       (pr_raw_tactic tac)));;
+	       (pr_glob_tactic tac)));;
 	  
 
 let rec path_to_first_error = function
@@ -421,7 +421,7 @@ let debug_tac = function
       	msgnl (fnl () ++
 	       str "=========    Successful tactic    =============" ++
                fnl () ++
-	       pr_raw_tactic compact_success_tac ++ fnl () ++
+	       pr_glob_tactic compact_success_tac ++ fnl () ++
 	       str "========= End of successful tactic ============");
       	result)
   | _ -> error "wrong arguments for debug_tac";;
@@ -462,7 +462,7 @@ let rec clean_path tac l =
   | _, _ -> failwith "this case should not happen in clean_path";;
 
 let rec report_error
-    : raw_tactic_expr -> goal sigma option ref -> raw_tactic_expr ref -> int list ref -> 
+    : glob_tactic_expr -> goal sigma option ref -> glob_tactic_expr ref -> int list ref -> 
       int list -> tactic =
   fun tac the_goal the_ast returned_path path -> 
     match tac with
@@ -523,12 +523,12 @@ let rec report_error
 		if !the_count > 1 then
 		  msgnl
 		    (str "in branch no " ++ int !the_count ++
-		     str " after tactic " ++ pr_raw_tactic a);
+		     str " after tactic " ++ pr_glob_tactic a);
 		raise e)
     | tac ->
 	(fun g ->
 	  try
-	   Tacinterp.interp tac g
+	   Tacinterp.eval_tactic tac g
 	  with
 	    e ->
 	      (the_ast := tac;
@@ -556,7 +556,7 @@ let descr_first_error tac =
 		    fnl () ++ str "on goal"  ++ fnl () ++
 		    pr_goal (sig_it (strip_some !the_goal)) ++ fnl () ++
 		    str "faulty tactic is" ++ fnl () ++ fnl () ++
-		    pr_raw_tactic ((*flatten_then*) !the_ast) ++ fnl ());
+		    pr_glob_tactic ((*flatten_then*) !the_ast) ++ fnl ());
 	     tclIDTAC g))
 
 (* TODO ... used ??
diff --git a/contrib/interface/debug_tac.mli b/contrib/interface/debug_tac.mli
index 05cef23aa7..ded714b629 100644
--- a/contrib/interface/debug_tac.mli
+++ b/contrib/interface/debug_tac.mli
@@ -1,6 +1,6 @@
 
-val report_error : Tacexpr.raw_tactic_expr ->
+val report_error : Tacexpr.glob_tactic_expr ->
     Proof_type.goal Proof_type.sigma option ref ->
-    Tacexpr.raw_tactic_expr ref -> int list ref -> int list -> Tacmach.tactic;;
+    Tacexpr.glob_tactic_expr ref -> int list ref -> int list -> Tacmach.tactic;;
 
-val clean_path : Tacexpr.raw_tactic_expr -> int list -> int list;;
+val clean_path : Tacexpr.glob_tactic_expr -> int list -> int list;;
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 9b1602ad41..4abcb5f96f 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -6,6 +6,7 @@ open Tactics;;
 open Tacticals;;
 open Hipattern;;
 open Pattern;;
+open Matching;;
 open Reduction;;
 open Rawterm;;
 open Environ;;
@@ -17,6 +18,7 @@ open Tacexpr;;
 open Typing;;
 open Pp;;
 open Libnames;;
+open Genarg;;
 open Topconstr;;
 
 let zz = (0,0);;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 8191a0978f..1fe718f0e5 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -598,10 +598,6 @@ let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
 	CT_coerce_TERM_CHANGE_to_TACTIC_ARG(CT_check_term(xlate_formula c))
     | MetaIdArg _ ->
 	xlate_error "MetaIdArg should only be used in quotations"
-    | MetaNumArg (_,n) ->
-	CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG 
-	  (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
-	     (CT_coerce_ID_to_ID_OR_INT(CT_metac (CT_int n))))
     | t ->
 	CT_coerce_TACTIC_COM_to_TACTIC_ARG(xlate_call_or_tacarg t)