diff options
Diffstat (limited to 'pretyping/namegen.mli')
| -rw-r--r-- | pretyping/namegen.mli | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index e23c6dad8..6702c9f70 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -13,10 +13,10 @@ open Environ (********************************************************************* Generating "intuitive" names from their type *) -val lowercase_first_char : identifier -> string +val lowercase_first_char : Id.t -> string val sort_hdchar : sorts -> string val hdchar : env -> types -> string -val id_of_name_using_hdchar : env -> types -> name -> identifier +val id_of_name_using_hdchar : env -> types -> name -> Id.t val named_hd : env -> types -> name -> name val mkProd_name : env -> name * types * types -> types @@ -40,27 +40,27 @@ val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr Fresh names *) (** Avoid clashing with a name satisfying some predicate *) -val next_ident_away_from : identifier -> (identifier -> bool) -> identifier +val next_ident_away_from : Id.t -> (Id.t -> bool) -> Id.t (** Avoid clashing with a name of the given list *) -val next_ident_away : identifier -> identifier list -> identifier +val next_ident_away : Id.t -> Id.t list -> Id.t (** Avoid clashing with a name already used in current module *) -val next_ident_away_in_goal : identifier -> identifier list -> identifier +val next_ident_away_in_goal : Id.t -> Id.t list -> 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 : identifier -> identifier list -> identifier +val next_global_ident_away : Id.t -> Id.t list -> Id.t (** Avoid clashing with a constructor name already used in current module *) -val next_name_away_in_cases_pattern : name -> identifier list -> identifier +val next_name_away_in_cases_pattern : name -> Id.t list -> Id.t -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 : name -> Id.t list -> Id.t (** default is "H" *) +val next_name_away_with_default : string -> name -> Id.t list -> + Id.t val next_name_away_with_default_using_types : string -> name -> - identifier list -> types -> identifier + Id.t list -> types -> Id.t val set_reserved_typed_name : (types -> name) -> unit @@ -75,10 +75,10 @@ type renaming_flags = val make_all_name_different : env -> env val compute_displayed_name_in : - renaming_flags -> identifier list -> name -> constr -> name * identifier list + renaming_flags -> Id.t list -> name -> constr -> name * Id.t list val compute_and_force_displayed_name_in : - renaming_flags -> identifier list -> name -> constr -> name * identifier list + renaming_flags -> Id.t list -> name -> constr -> name * Id.t list val compute_displayed_let_name_in : - renaming_flags -> identifier list -> name -> constr -> name * identifier list + renaming_flags -> Id.t list -> name -> constr -> name * Id.t list val rename_bound_vars_as_displayed : - identifier list -> name list -> types -> types + Id.t list -> name list -> types -> types |