A new step on using alpha-conversion in printing notations.

A couple of bugs have been found.

Example #4932 is now printing correctly in the presence of multiple
binders (when no let-in, no irrefutable patterns).

2 files changed, 23 insertions, 5 deletions

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 244f013e3c..51660818f4 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -487,14 +487,24 @@ let update_subst na l =
      else na,l)
     na (na,l)
 
+exception UnsoundRenaming
+
+let rename_var l id =
+  try
+    let id' = Id.List.assoc id l in
+    (* Check that no other earlier binding hide the one found *)
+    let _,(id'',_) = List.extract_first (fun (_,id) -> Id.equal id id') l in
+    if Id.equal id id'' then id' else raise UnsoundRenaming
+  with Not_found ->
+    if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
+    else id
+
 let rec rename_glob_vars l = function
   | GVar (loc,id) as r ->
-     (try GVar (loc,Id.List.assoc id l)
-      with Not_found ->
-      if List.exists (fun (_,id') -> Id.equal id id') l then raise Not_found
-      else r)
+      let id' = rename_var l id in
+      if id == id' then r else GVar (loc,id')
   | GRef (_,VarRef id,_) as r ->
-      if List.exists (fun (_,id') -> Id.equal id id') l then raise Not_found
+      if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
       else r
   | GProd (loc,na,bk,t,c) ->
       let na',l' = update_subst na l in
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index dcc6ef88b9..55e6b6533f 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -44,6 +44,14 @@ val bound_glob_vars : glob_constr -> Id.Set.t
 val loc_of_glob_constr : glob_constr -> Loc.t
 val glob_visible_short_qualid : glob_constr -> Id.t list
 
+(* Renaming free variables using a renaming map; fails with
+   [UnsoundRenaming] if applying the renaming would introduce
+   collision, as in, e.g., renaming [P x y] using substitution [(x,y)];
+   inner alpha-conversion done only for forall, fun, let but
+   not for cases and fix *)
+
+exception UnsoundRenaming
+val rename_var : (Id.t * Id.t) list -> Id.t -> Id.t
 val rename_glob_vars : (Id.t * Id.t) list -> glob_constr -> glob_constr
 
 (** [map_pattern_binders f m c] applies [f] to all the binding names