diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 3 | ||||
| -rw-r--r-- | plugins/xml/dumptree.ml4 | 4 |
3 files changed, 5 insertions, 4 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index b5a2ac82eb..fd98d54579 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -29,7 +29,7 @@ let pr_goal gs = (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), (str "thesis := " ++ fnl ()), Printer.pr_context_of env, - Printer.pr_ltype_env_at_top env (Goal.V82.concl sigma g) + Printer.pr_goal_concl_style_env env (Goal.V82.concl sigma g) in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 0f92378d68..872d3be4ac 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -128,7 +128,8 @@ let pf_get_new_ids idl g = [] let compute_renamed_type gls c = - rename_bound_vars_as_displayed [] (pf_type_of gls c) + rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] + (pf_type_of gls c) let h'_id = id_of_string "h'" let heq_id = id_of_string "Heq" let teq_id = id_of_string "teq" diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index 69b9e6ea72..8415bbd10d 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>") |