aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml/dumptree.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/xml/dumptree.ml4')
-rw-r--r--plugins/xml/dumptree.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 82e90876d..9419ba597 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -116,7 +116,7 @@ let pr_subgoal_metas_xml metas env=
;;
let pr_goal_xml g =
- let env = try evar_env g with _ -> empty_env in
+ let env = try evar_unfiltered_env g with _ -> empty_env in
if g.evar_extra = None then
(hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++
xmlstream (pr_ltype_env_at_top env g.evar_concl) ++