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).

1 files changed, 15 insertions, 5 deletions

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 244f013e3..51660818f 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