From 744e7f6a319f4d459a3cc2309f575d43041d75aa Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 16 Oct 2006 17:11:44 +0000
Subject: affichage des ... dans les scripts

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9244 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/xml/proofTree2Xml.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib/xml')

diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index d382ef955c..dbdc79a802 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -141,7 +141,7 @@ Pp.ppnl (Pp.(++) (Pp.str
               (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
 
      | {PT.goal=goal;
-        PT.ref=Some(PT.Nested (PT.Tactic tactic_expr,hidden_proof),nodes)} ->
+        PT.ref=Some(PT.Nested (PT.Tactic(tactic_expr,_),hidden_proof),nodes)} ->
          (* [hidden_proof] is the proof of the tactic;                     *)
          (* [nodes] are the proof of the subgoals generated by the tactic; *)
          (* [flat_proof] if the proof-tree obtained substituting [nodes]   *)
-- 
cgit v1.2.3