diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-20 14:05:55 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-20 14:05:55 +0000 |
| commit | 929885b46d19cb8e90507bf2f6bddc146a0458a9 (patch) | |
| tree | 74c5c0465a2d6f492d1ab557672c0e3d7f05fd57 /plugins/xml | |
| parent | d288152f7d886ca6dba3944d20c6ca21452533da (diff) | |
Fixing alpha-conversion bug #2723 introduced in r12485-12486.
The optimisation done of Namegen.visibly_occur_id did not preserve
the previous behavior when pr_constr/constr_extern/detype were
called on a term with free rel variables. We backtrack on it to
go back to the 8.2 behavior.
Seized this opportunity to clarify the meaning of the at_top flag
in constrextern.ml and printer.ml and to rename it into
goal_concl_style. The badly-named at_top flag was introduced in
Coq 6.3 in 1999 to mean that when printing variables bound in the
goal, names had to avoid the names of the variables of the goal
context, so as to keep naming stable when using "intro"; in
r4458, printing improved by not avoiding names that were short
names of global definitions, e.g. "S", or "O" (except when the
at_top flag was on for compatibility reasons).
Other printing strategies could be possible in the
non-goal-concl-style mode. For instance, all bound variables
could be made distinct in a given expression, even if no clash
occur, therefore following so-called Barendregt's
convention. This could be done by setting "avoid"
to "ids_of_rel_context (rel_context env)" in extern_constr and
extern_type (and then, Namegen.visibly_occur_id could be
re-simplified again!).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15067 85f007b7-540e-0410-9357-904b9bb8a0f7
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 69b9e6ea7..8415bbd10 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>") |