aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml/proofTree2Xml.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/xml/proofTree2Xml.ml4')
-rw-r--r--plugins/xml/proofTree2Xml.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index b0e4fcc69..2f5eb6ac2 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
@@ -144,7 +144,7 @@ Pp.ppnl (Pp.(++) (Pp.str
Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node
in begin
match tactic_expr with
- | T.TacArg (T.Tacexp _) ->
+ | T.TacArg (_,T.Tacexp _) ->
(* We don't need to keep the level of abstraction introduced at *)
(* user-level invocation of tactic... (see Tacinterp.hide_interp)*)
aux flat_proof old_hyps