diff options
| author | herbelin | 2004-03-24 18:14:18 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-24 18:14:18 +0000 |
| commit | af0ce2cc07f0dc903d0abb4518f2b23ff5299034 (patch) | |
| tree | 235db3b1ac535f96f18b512ebde3326458164ec8 | |
| parent | 5332a2c2b3e7d8d41dd40c75ff44496bb9c25c8f (diff) | |
Utilisation du printer approprie a la version de syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5551 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index 4a568da36f..6016937d07 100644 --- a/contrib/xml/proofTree2Xml.ml4 +++ b/contrib/xml/proofTree2Xml.ml4 @@ -141,7 +141,8 @@ Pp.ppnl (Pp.(++) (Pp.str aux flat_proof old_hyps | _ -> (****** la tactique employee *) - let tac = std_ppcmds_to_string (Pptactic.pr_tactic tactic_expr) in + let prtac = if !Options.v7 then Pptactic.pr_tactic else 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 |