diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
| commit | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch) | |
| tree | d88d05baf35b9b09a034233300f35a694f9fa6c2 /plugins/xml | |
| parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) | |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'plugins/xml')
| -rw-r--r-- | plugins/xml/dumptree.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index 3c3e54fa..56ce7ef2 100644 --- a/plugins/xml/dumptree.ml4 +++ b/plugins/xml/dumptree.ml4 @@ -107,7 +107,7 @@ let pr_context_xml env = let pr_subgoal_metas_xml metas env= let pr_one (meta, typ) = - fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_ltype_env_at_top env typ) ++ + fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_goal_concl_style_env env typ) ++ str "\"/>" in List.fold_left (++) (mt ()) (List.map pr_one metas) @@ -117,7 +117,7 @@ let pr_goal_xml sigma g = let env = try Goal.V82.unfiltered_env sigma g with _ -> empty_env in if Decl_mode.try_get_info sigma g = None then (hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++ - xmlstream (pr_ltype_env_at_top env (Goal.V82.concl sigma g)) ++ + xmlstream (pr_goal_concl_style_env env (Goal.V82.concl sigma g)) ++ str "\"/>" ++ (pr_context_xml env)) ++ fnl () ++ str "</goal>") |