diff options
Diffstat (limited to 'engine/namegen.mli')
| -rw-r--r-- | engine/namegen.mli | 7 |
1 files changed, 6 insertions, 1 deletions
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 *) |