Merge PR #1040: Efficient fresh name generation

1 files changed, 10 insertions, 11 deletions

diff --git a/engine/namegen.mli b/engine/namegen.mli
index 14846a9184..6fde90a39c 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -72,23 +72,22 @@ val next_ident_away_from : Id.t -> (Id.t -> bool) -> Id.t
     the whole identifier except for the {i subscript}.
 
     E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *)
-val next_ident_away : Id.t -> Id.t list -> Id.t
+val next_ident_away : Id.t -> Id.Set.t -> Id.t
 
 (** Avoid clashing with a name already used in current module *)
-val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t
+val next_ident_away_in_goal : Id.t -> Id.Set.t -> Id.t
 
 (** Avoid clashing with a name already used in current module 
    but tolerate overwriting section variables, as in goals *)
-val next_global_ident_away : Id.t -> Id.t list -> Id.t
+val next_global_ident_away : Id.t -> Id.Set.t -> Id.t
 
 (** Default is [default_non_dependent_ident] *)
-val next_name_away  : Name.t -> Id.t list -> Id.t
+val next_name_away  : Name.t -> Id.Set.t -> Id.t
 
-val next_name_away_with_default : string -> Name.t -> Id.t list ->
-  Id.t
+val next_name_away_with_default : string -> Name.t -> Id.Set.t -> Id.t
 
 val next_name_away_with_default_using_types : string -> Name.t ->
-  Id.t list -> types -> Id.t
+  Id.Set.t -> types -> Id.t
 
 val set_reserved_typed_name : (types -> Name.t) -> unit
 
@@ -103,13 +102,13 @@ type renaming_flags =
 val make_all_name_different : env -> evar_map -> env
 
 val compute_displayed_name_in :
-  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
 val compute_and_force_displayed_name_in :
-  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  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.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
 val rename_bound_vars_as_displayed :
-  evar_map -> Id.t list -> Name.t list -> types -> types
+  evar_map -> Id.Set.t -> Name.t list -> types -> types
 
 (**********************************************************************)
 (* Naming strategy for arguments in Prop when eliminating inductive types *)