Fixing #5401 (printing of patterns with bound anonymous variables).

This fixes also #5731, #6035, #5364.

1 files changed, 10 insertions, 3 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index 2e62b8901..a38c73ed0 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -376,15 +376,22 @@ let next_name_for_display sigma flags =
   | RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
-let compute_displayed_name_in sigma flags avoid na c =
+let compute_displayed_name_in_gen_poly noccurn_fun sigma flags avoid na c =
   match na with
-  | Anonymous when noccurn sigma 1 c ->
+  | Anonymous when noccurn_fun sigma 1 c ->
     (Anonymous,avoid)
   | _ ->
     let fresh_id = next_name_for_display sigma flags na avoid in
-    let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in
+    let idopt = if noccurn_fun sigma 1 c then Anonymous else Name fresh_id in
     (idopt, Id.Set.add fresh_id avoid)
 
+let compute_displayed_name_in = compute_displayed_name_in_gen_poly noccurn
+
+let compute_displayed_name_in_gen f sigma =
+  (* only flag which does not need a constr, maybe to be refined *)
+  let flag = RenamingForGoal in
+  compute_displayed_name_in_gen_poly f sigma flag
+
 let compute_and_force_displayed_name_in sigma flags avoid na c =
   match na with
   | Anonymous when noccurn sigma 1 c ->