From d03b0e0740379b72f3e14d397378c1b02867714c Mon Sep 17 00:00:00 2001
From: cek
Date: Wed, 7 Oct 2009 09:04:51 +0000
Subject: Fix for missing hypotesae in XML proof tree export.

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

(limited to 'plugins/xml')

diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 82e90876de..9419ba597e 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) ++
-- 
cgit v1.2.3