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

2 files changed, 20 insertions, 15 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 3d2f3e0891..dd17ee0c8a 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -36,13 +36,19 @@ let delayed_emacs_cmd s =
 (**********************************************************************)
 (** Terms                                                             *)
 
-  (* [at_top] means ids of env must be avoided in bound variables *)
-let pr_constr_core at_top env t =
-  pr_constr_expr (extern_constr at_top env t)
-let pr_lconstr_core at_top env t =
-  pr_lconstr_expr (extern_constr at_top env t)
+(* [goal_concl_style] means that all names of goal/section variables
+   and all names of rel variables (if any) in the given env and all short
+   names of global definitions of the current module must be avoided while
+   printing bound variables.
+   Otherwise, short names of global definitions are printed qualified
+   and only names of goal/section variables and rel names that do
+   _not_ occur in the scope of the binder to be printed are avoided. *)
+
+let pr_constr_core goal_concl_style env t =
+  pr_constr_expr (extern_constr goal_concl_style env t)
+let pr_lconstr_core goal_concl_style env t =
+  pr_lconstr_expr (extern_constr goal_concl_style env t)
 
-let pr_lconstr_env_at_top env = pr_lconstr_core true env
 let pr_lconstr_env env = pr_lconstr_core false env
 let pr_constr_env env = pr_constr_core false env
 
@@ -69,12 +75,12 @@ let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_en
 let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c
 let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c
 
-let pr_type_core at_top env t =
-  pr_constr_expr (extern_type at_top env t)
-let pr_ltype_core at_top env t =
-  pr_lconstr_expr (extern_type at_top env t)
+let pr_type_core goal_concl_style env t =
+  pr_constr_expr (extern_type goal_concl_style env t)
+let pr_ltype_core goal_concl_style env t =
+  pr_lconstr_expr (extern_type goal_concl_style env t)
 
-let pr_ltype_env_at_top env = pr_ltype_core true env
+let pr_goal_concl_style_env env = pr_ltype_core true env
 let pr_ltype_env env = pr_ltype_core false env
 let pr_type_env env = pr_type_core false env
 
@@ -263,7 +269,7 @@ let default_pr_goal gs =
   let preamb,thesis,penv,pc =
     mt (), mt (),
     pr_context_of env,
-    pr_ltype_env_at_top env (Goal.V82.concl sigma g)
+    pr_goal_concl_style_env env (Goal.V82.concl sigma g)
   in
     preamb ++
     str"  " ++ hv 0 (penv ++ fnl () ++
@@ -280,7 +286,7 @@ let pr_goal_tag g =
 let pr_concl n sigma g =
   let (g,sigma) = Goal.V82.nf_evar sigma g in
   let env = Goal.V82.env sigma g in
-  let pc = pr_ltype_env_at_top env (Goal.V82.concl sigma g) in
+  let pc = pr_goal_concl_style_env env (Goal.V82.concl sigma g) in
     str (emacs_str "")  ++
       str "subgoal " ++ int n ++ pr_goal_tag g ++
       str " is:" ++ cut () ++ str" "  ++ pc
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 2d437c2013..bbc3a6cad1 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -26,7 +26,6 @@ open Tacexpr
 (** Terms *)
 
 val pr_lconstr_env         : env -> constr -> std_ppcmds
-val pr_lconstr_env_at_top  : env -> constr -> std_ppcmds
 val pr_lconstr             : constr -> std_ppcmds
 
 val pr_constr_env          : env -> constr -> std_ppcmds
@@ -44,7 +43,7 @@ val pr_constr_under_binders      : constr_under_binders -> std_ppcmds
 val pr_lconstr_under_binders_env : env -> constr_under_binders -> std_ppcmds
 val pr_lconstr_under_binders     : constr_under_binders -> std_ppcmds
 
-val pr_ltype_env_at_top    : env -> types -> std_ppcmds
+val pr_goal_concl_style_env : env -> types -> std_ppcmds
 val pr_ltype_env           : env -> types -> std_ppcmds
 val pr_ltype               : types -> std_ppcmds