diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-06 10:08:32 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-06 10:08:32 +0000 |
| commit | 1f05de5d4e19867c3425c39999a1f58e12b57657 (patch) | |
| tree | 8efa17000b77b1d39c07bbfeb9da7153181f70f6 /plugins/xml | |
| parent | a0057a6657f5615c3d3448fae10b26a968d30fe1 (diff) | |
Clean-up : removal of Proof_type.tactic_expr
This instance of gen_tactic_expr was used only to decorate
tactics via Refiner.abstract_tactics and alii, but these
expressions are now ignored by the new proof-engine (no "info"...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15865 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml')
| -rw-r--r-- | plugins/xml/dumptree.ml4 | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index c0c8ada95..1fd829e7a 100644 --- a/plugins/xml/dumptree.ml4 +++ b/plugins/xml/dumptree.ml4 @@ -36,15 +36,6 @@ let thin_sign osign sign = sign ~init:Environ.empty_named_context_val ;; -let pr_tactic_xml = function - | TacArg (_,Tacexp t) -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_glob_tactic (Global.env()) t) ++ str "\"/>" - | t -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_tactic (Global.env()) t) ++ str "\"/>" -;; - -let pr_proof_instr_xml instr = - Ppdecl_proof.pr_proof_instr (Global.env()) instr -;; - let pr_var_decl_xml env (id,c,typ) = let ptyp = print_constr_env env typ in match c with |