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

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

2 files changed, 16 insertions, 4 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 ->
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 6fde90a39..d29b69259 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -106,10 +106,15 @@ val compute_displayed_name_in :
 val compute_and_force_displayed_name_in :
   evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
 val compute_displayed_let_name_in :
-  evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
+  evar_map -> renaming_flags -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t
 val rename_bound_vars_as_displayed :
   evar_map -> Id.Set.t -> Name.t list -> types -> types
 
+(* Generic function expecting a "not occurn" function *)
+val compute_displayed_name_in_gen :
+  (evar_map -> int -> 'a -> bool) ->
+  evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t
+
 (**********************************************************************)
 (* Naming strategy for arguments in Prop when eliminating inductive types *)