diff options
Diffstat (limited to 'contrib/xml/proofTree2Xml.ml4')
| -rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index b9d920903..698c732d2 100644 --- a/contrib/xml/proofTree2Xml.ml4 +++ b/contrib/xml/proofTree2Xml.ml4 @@ -156,7 +156,7 @@ Pp.ppnl (Pp.(++) (Pp.str aux flat_proof old_hyps | _ -> (****** la tactique employee *) - let prtac = if !Options.v7 then Pptactic.pr_tactic else Pptacticnew.pr_tactic (Global.env()) in + let prtac = Pptacticnew.pr_tactic (Global.env()) in let tac = std_ppcmds_to_string (prtac tactic_expr) in let tacname= first_word tac in let of_attribute = ("name",tacname)::("script",tac)::of_attribute in |