diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 28 |
1 files changed, 0 insertions, 28 deletions
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 |