4 files changed, 1 insertions, 37 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 9d1a9eeaf..69798a6d2 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -633,7 +633,7 @@ and intern_tactic_seq onlytac ist = function
 
 and intern_tactic_as_arg loc onlytac ist a =
   match intern_tacarg !strict_check onlytac ist a with
-  | TacCall _ | TacExternal _ | Reference _
+  | TacCall _ | Reference _
   | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a)
   | Tacexp a -> a
   | ConstrMayEval _ | UConstr _ | TacFreshId _ | TacPretype _ | TacNumgoals as a ->
@@ -664,8 +664,6 @@ and intern_tacarg strict onlytac ist = function
       TacCall (loc,
         intern_applied_tactic_reference ist f,
         List.map (intern_tacarg !strict_check false ist) l)
-  | TacExternal (loc,com,req,la) ->
-      TacExternal (loc,com,req,List.map (intern_tacarg !strict_check false ist) la)
   | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x)
   | TacPretype c -> TacPretype (intern_constr ist c)
   | TacNumgoals -> TacNumgoals
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c3869ec29..85d0ac4cd 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
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 8c639cb18..54e604fe4 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -103,10 +103,6 @@ val interp : raw_tactic_expr -> unit Proofview.tactic
 
 val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic
 
-(** Declare the xml printer *)
-val declare_xml_printer :
-  (out_channel -> Environ.env -> Evd.evar_map -> constr -> unit) -> unit
-
 (** Internals that can be useful for syntax extensions. *)
 
 val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> Id.t Loc.located -> 'a
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index ab96fe674..b1d03f86e 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -258,8 +258,6 @@ and subst_tacarg subst = function
   | MetaIdArg (_loc,_,_) -> assert false
   | TacCall (_loc,f,l) ->
       TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l)
-  | TacExternal (_loc,com,req,la) ->
-      TacExternal (_loc,com,req,List.map (subst_tacarg subst) la)
   | TacFreshId _ as x -> x
   | TacPretype c -> TacPretype (subst_glob_constr subst c)
   | TacNumgoals -> TacNumgoals