diff options
Diffstat (limited to 'pretyping/namegen.mli')
| -rw-r--r-- | pretyping/namegen.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index 0c9fc4f6b..637cbf64d 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -59,6 +59,11 @@ val next_name_away : name -> identifier list -> identifier (** default is "H" * val next_name_away_with_default : string -> name -> identifier list -> identifier +val next_name_away_with_default_using_types : string -> name -> + identifier list -> types -> identifier + +val set_reserved_typed_name : (types -> name) -> unit + (********************************************************************* Making name distinct for displaying *) |