Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous variables).

1 files changed, 6 insertions, 1 deletions

diff --git a/engine/namegen.mli b/engine/namegen.mli
index 6fde90a39c..d29b69259f 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 *)