diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-28 20:07:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-28 20:26:46 +0200 |
| commit | de7d2fdb97975dcd94005bb6fa79a312c8afa017 (patch) | |
| tree | d2739984aa3f2090c17b9d18f884f1986c52dff0 /engine/namegen.mli | |
| parent | e5659c8ffe735c530a707a61c692a3af21a79a9a (diff) | |
Fixing #5401 (printing of patterns with bound anonymous variables).
This fixes also #5731, #6035, #5364.
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 *) |