package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type intro_pattern_naming_expr =
  1. | IntroIdentifier of Names.Id.t
  2. | IntroFresh of Names.Id.t
  3. | IntroAnonymous
val intro_pattern_naming_eq : intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool
val default_prop_ident : Names.Id.t
val default_small_ident : Names.Id.t
val default_type_ident : Names.Id.t
val default_non_dependent_ident : Names.Id.t
val default_dependent_ident : Names.Id.t
val lowercase_first_char : Names.Id.t -> string
val sort_hdchar : Sorts.t -> string
val hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> string
val id_of_name_using_hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t -> Names.Id.t
val head_name : Evd.evar_map -> EConstr.types -> Names.Id.t option
val it_mkProd_or_LetIn_name : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.rel_context -> EConstr.types
val it_mkLambda_or_LetIn_name : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.rel_context -> EConstr.constr
val next_ident_away_from : Names.Id.t -> (Names.Id.t -> bool) -> Names.Id.t
val next_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t
val next_ident_away_in_goal : Names.Id.t -> Names.Id.Set.t -> Names.Id.t
val next_global_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t
val next_name_away : Names.Name.t -> Names.Id.Set.t -> Names.Id.t
val next_name_away_with_default : string -> Names.Name.t -> Names.Id.Set.t -> Names.Id.t
val next_name_away_with_default_using_types : string -> Names.Name.t -> Names.Id.Set.t -> EConstr.types -> Names.Id.t
val set_reserved_typed_name : (EConstr.types -> Names.Name.t) -> unit
type renaming_flags =
  1. | RenamingForCasesPattern of Names.Name.t list * EConstr.constr
  2. | RenamingForGoal
  3. | RenamingElsewhereFor of Names.Name.t list * EConstr.constr
val make_all_name_different : Environ.env -> Evd.evar_map -> Environ.env
val compute_and_force_displayed_name_in : Evd.evar_map -> renaming_flags -> Names.Id.Set.t -> Names.Name.t -> EConstr.constr -> Names.Name.t * Names.Id.Set.t
val compute_displayed_let_name_in : Evd.evar_map -> renaming_flags -> Names.Id.Set.t -> Names.Name.t -> 'a -> Names.Name.t * Names.Id.Set.t
val rename_bound_vars_as_displayed : Evd.evar_map -> Names.Id.Set.t -> Names.Name.t list -> EConstr.types -> EConstr.types
val compute_displayed_name_in_gen : (Evd.evar_map -> int -> 'a -> bool) -> Evd.evar_map -> Names.Id.Set.t -> Names.Name.t -> 'a -> Names.Name.t * Names.Id.Set.t
val set_mangle_names_mode : Names.Id.t -> unit