Removing the XML plugin.

Left a README, just in case someone will discover the remnants of it
decades from now.

1 files changed, 0 insertions, 28 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c3869ec293..85d0ac4cd7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -221,23 +221,6 @@ let coerce_to_tactic loc id v =
     | _ -> fail ()
   else fail ()
 
-(* External tactics *)
-let print_xml_term = ref (fun _ -> failwith "print_xml_term unset")
-let declare_xml_printer f = print_xml_term := f
-
-let internalise_tacarg ch = G_xml.parse_tactic_arg ch
-
-let extern_tacarg ch env sigma v = match Value.to_constr v with
-| None ->
-  error "Only externing of closed terms is implemented."
-| Some c -> !print_xml_term ch env sigma c
-
-let extern_request ch req gl la =
-  output_string ch "<REQUEST req=\""; output_string ch req;
-  output_string ch "\">\n";
-  List.iter (pf_apply (extern_tacarg ch) gl) la;
-  output_string ch "</REQUEST>\n"
-
 let value_of_ident id =
   in_gen (topwit wit_intro_pattern)
     (Loc.ghost, IntroNaming (IntroIdentifier id))
@@ -1317,10 +1300,6 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
       interp_ltac_reference loc true ist f >>= fun fv ->
       Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs ->
       interp_app loc ist fv largs
-  | TacExternal (loc,com,req,la) ->
-      let (>>=) = Ftactic.bind in
-      Ftactic.List.map (fun a -> interp_tacarg ist a) la >>= fun la_interp ->
-      interp_external loc ist com req la_interp
   | TacFreshId l ->
       Ftactic.enter begin fun gl ->
         let id = interp_fresh_id ist (Tacmach.New.pf_env gl) l in
@@ -1522,13 +1501,6 @@ and interp_match_goal ist lz lr lmr =
       interp_match_successes lz ist (TacticMatching.match_goal env sigma hyps concl ilr)
     end
 
-and interp_external loc ist com req la =
-  Ftactic.nf_enter begin fun gl ->
-  let f ch = Tacmach.New.of_old (fun gl -> extern_request ch req gl la) gl in
-  let g ch = internalise_tacarg ch in
-  interp_tacarg ist (System.connect f g com)
-  end
-
 (* Interprets extended tactic generic arguments *)
 (* spiwack: interp_genarg has an argument [concl] for the case of
    "casted open constr". And [gl] for [Geninterp]. I haven't changed