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

13 files changed, 73 insertions, 137 deletions

diff --git a/contrib/correctness/pmlize.ml b/contrib/correctness/pmlize.ml
index ed2896ec90..5c6e845a36 100644
--- a/contrib/correctness/pmlize.ml
+++ b/contrib/correctness/pmlize.ml
@@ -14,6 +14,7 @@ open Names
 open Term
 open Termast
 open Pattern
+open Matching
 
 open Pmisc
 open Ptype
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 9e3e8a1bbb..888f876dee 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -485,8 +485,8 @@ GEXTEND Gram
   END
 ;;
 
-let wit_prog, rawwit_prog = Genarg.create_arg "PROGRAMS-PROG"
-let wit_typev, rawwit_typev = Genarg.create_arg "PROGRAMS-TYPEV"
+let wit_prog, _, rawwit_prog = Genarg.create_arg "PROGRAMS-PROG"
+let wit_typev, _, rawwit_typev = Genarg.create_arg "PROGRAMS-TYPEV"
 
 open Pp
 open Util
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index 5aa497d7f8..eb64b7eb2b 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -16,6 +16,7 @@ open Nameops
 open Term
 open Termops
 open Pattern
+open Matching
 open Environ
 
 open Pmisc
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 0c908e1ad8..c502ea9b01 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -89,38 +89,43 @@ open Extend
 open Pcoq
 open Genarg
 
-let wit_minus_div_arg, rawwit_minus_div_arg = Genarg.create_arg "minus_div_arg"
-let minus_div_arg = create_generic_entry "minus_div_arg" rawwit_minus_div_arg
-let _ = Tacinterp.add_genarg_interp "minus_div_arg"
-  (fun ist gl x ->
-    (in_gen wit_minus_div_arg
-      (out_gen (wit_pair (wit_opt wit_constr) (wit_opt wit_constr))
-	(Tacinterp.genarg_interp ist gl
-	  (in_gen (wit_pair (wit_opt rawwit_constr) (wit_opt rawwit_constr))
-	    (out_gen rawwit_minus_div_arg x))))))
+VERNAC ARGUMENT EXTEND divarg
+| [ "div" ":=" constr(adiv) ] -> [ adiv ]
+END
+
+VERNAC ARGUMENT EXTEND minusarg
+| [ "minus" ":=" constr(aminus) ] -> [ aminus ]
+END
 
+(*
+(* The v7->v8 translator needs printers, then temporary use ARGUMENT EXTEND...*)
+VERNAC ARGUMENT EXTEND minus_div_arg
+| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
+| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
+| [ ] -> [ None, None ]
+END
+*)
+
+(* For the translator, otherwise the code above is OK *)
 open Ppconstrnew
-let pp_minus_div_arg (omin,odiv) = str "still no printer for minus_div_arg"
-let pp_raw_minus_div_arg (omin,odiv) =
+let pp_minus_div_arg _prc _prt (omin,odiv) = 
   if omin=None && odiv=None then mt() else
     spc() ++ str "with" ++
-    pr_opt (fun c -> str "minus := " ++ pr_constr c) omin ++
-    pr_opt (fun c -> str "div := " ++ pr_constr c) odiv
-
+    pr_opt (fun c -> str "minus := " ++ _prc c) omin ++
+    pr_opt (fun c -> str "div := " ++ _prc c) odiv
+(*
 let () =
   Pptactic.declare_extra_genarg_pprule true
-    (rawwit_minus_div_arg,pp_raw_minus_div_arg)
+    (rawwit_minus_div_arg,pp_minus_div_arg)
+    (globwit_minus_div_arg,pp_minus_div_arg)
     (wit_minus_div_arg,pp_minus_div_arg)
-
-open Pcoq.Constr
-GEXTEND Gram
-  GLOBAL: minus_div_arg;
-  minus_arg: [ [ IDENT "minus"; ":="; aminus = constr -> aminus ] ];
-  div_arg: [ [ IDENT "div"; ":="; adiv = constr -> adiv ] ];
-  minus_div_arg:
-    [ [ "with"; m = minus_arg; d = OPT div_arg -> Some m, d
-      | "with"; d = div_arg; m = OPT minus_arg -> m, Some d
-      | -> None, None ] ];
+*)
+ARGUMENT EXTEND minus_div_arg 
+  TYPED AS constr_opt * constr_opt
+  PRINTED BY pp_minus_div_arg
+| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
+| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
+| [ ] -> [ None, None ]
 END
 
 VERNAC COMMAND EXTEND Field
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)
 
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 393eff193f..270f09587f 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -109,6 +109,7 @@ open Names
 open Term
 open Instantiate
 open Pattern
+open Matching
 open Tacmach
 open Tactics
 open Proof_trees
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4
index 2807a3d6ee..da65de2376 100644
--- a/contrib/xml/xmlentries.ml4
+++ b/contrib/xml/xmlentries.ml4
@@ -32,54 +32,18 @@ open Pcoq;;
 
 (* File name *)
 
-let wit_filename, rawwit_filename = Genarg.create_arg "filename"
-let filename = Pcoq.create_generic_entry "filename" rawwit_filename
-let _ = Tacinterp.add_genarg_interp "filename"
-  (fun ist gl x ->
-    (in_gen wit_filename
-      (out_gen (wit_opt wit_string)
-	(Tacinterp.genarg_interp ist gl
-	  (in_gen (wit_opt rawwit_string)
-	    (out_gen rawwit_filename x))))))
-
-GEXTEND Gram
-  GLOBAL: filename;
-  filename: [ [ IDENT "File"; fn = STRING -> Some fn | -> None ] ];
+VERNAC ARGUMENT EXTEND filename
+| [ "File" string(fn) ] -> [ Some fn ]
+| [ ] -> [ None ]
 END
 
-let pr_filename = function Some fn -> str " File" ++ str fn | None -> mt ()
-
-let _ = 
-  Pptactic.declare_extra_genarg_pprule true
-    (rawwit_filename, pr_filename)
-    (wit_filename, pr_filename)
-
 (* Disk name *)
 
-let wit_diskname, rawwit_diskname = Genarg.create_arg "diskname"
-let diskname = create_generic_entry "diskname" rawwit_diskname
-let _ = Tacinterp.add_genarg_interp "diskname"
-  (fun ist gl x ->
-    (in_gen wit_diskname
-      (out_gen (wit_opt wit_string)
-	(Tacinterp.genarg_interp ist gl
-	  (in_gen (wit_opt rawwit_string)
-	    (out_gen rawwit_diskname x))))))
-
-GEXTEND Gram
-  GLOBAL: diskname;
-  diskname: [ [ IDENT "Disk"; fn = STRING -> Some fn | -> None ] ];
+VERNAC ARGUMENT EXTEND diskname
+| [ "Disk" string(fn) ] -> [ Some fn ]
+| [ ] -> [ None ]
 END
 
-open Pp
-
-let pr_diskname = function Some fn -> str " Disk" ++ str fn | None -> mt ()
-
-let _ = 
-  Pptactic.declare_extra_genarg_pprule true
-    (rawwit_diskname, pr_diskname)
-    (wit_diskname, pr_diskname)
-
 VERNAC COMMAND EXTEND Xml
 | [ "Print" "XML" filename(fn) global(id) ] -> [ Xmlcommand.print id fn ]
 
@@ -95,39 +59,3 @@ VERNAC COMMAND EXTEND Xml
     [ Xmlcommand.printSection id dn ]
 *)
 END
-(*
-vinterp_add "Print"
- (function
-     [VARG_QUALID id] ->
-        (fun () -> Xmlcommand.print id None)
-   | [VARG_QUALID id ; VARG_STRING fn] ->
-        (fun () -> Xmlcommand.print id (Some fn))
-   | _ -> anomaly "This should be trapped");;
-
-vinterp_add "Show"
- (function
-     [] ->
-        (fun () -> Xmlcommand.show None)
-   | [VARG_STRING fn] ->
-        (fun () -> Xmlcommand.show (Some fn))
-   | _ -> anomaly "This should be trapped");;
-
-vinterp_add "XmlPrintAll"
- (function
-     [] -> (fun () -> Xmlcommand.printAll ())
-   | _  -> anomaly "This should be trapped");;
-
-vinterp_add "XmlPrintModule"
- (function
-     [VARG_QUALID id] -> (fun () -> Xmlcommand.printModule id None)
-   | [VARG_QUALID id ; VARG_STRING dn] ->
-        (fun () -> Xmlcommand.printModule id (Some dn))
-   | _  -> anomaly "This should be trapped");;
-
-vinterp_add "XmlPrintSection"
- (function
-     [VARG_IDENTIFIER id] -> (fun () -> Xmlcommand.printSection id None)
-   | [VARG_IDENTIFIER id ; VARG_STRING dn] ->
-        (fun () -> Xmlcommand.printSection id (Some dn))
-   | _  -> anomaly "This should be trapped");;
-*)