package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c

doc/coq-core.engine/Namegen/index.html

Module NamegenSource

This file features facilities to generate fresh names.

Sourcetype intro_pattern_naming_expr =
  1. | IntroIdentifier of Names.Id.t
  2. | IntroFresh of Names.Id.t
  3. | IntroAnonymous

General evar naming using intro patterns

Sourceval intro_pattern_naming_eq : intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool

Equalities on intro_pattern_naming

Sourceval default_prop_ident : Names.Id.t
Sourceval default_small_ident : Names.Id.t
Sourceval default_type_ident : Names.Id.t
Sourceval default_non_dependent_ident : Names.Id.t
Sourceval default_dependent_ident : Names.Id.t
Sourceval lowercase_first_char : Names.Id.t -> string
Sourceval sort_hdchar : Sorts.t -> string
Sourceval hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> string
Sourceval id_of_name_using_hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t -> Names.Id.t
Sourceval head_name : Evd.evar_map -> EConstr.types -> Names.Id.t option

Deprecated synonyms of mkProd_name and mkLambda_name

Sourceval next_ident_away_from : Names.Id.t -> (Names.Id.t -> bool) -> Names.Id.t

Avoid clashing with a name satisfying some predicate

Sourceval next_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t

next_ident_away original_id unwanted_ids returns a new identifier as close as possible to the original_id while avoiding all unwanted_ids.

In particular:

  • if original_id does not appear in the list of unwanted_ids, then original_id is returned.

  • if original_id appears in the list of unwanted_ids, then this function returns a new id that:

    • has the same root as the original_id,
    • does not occur in the list of unwanted_ids,
    • has the smallest possible subscript.

where by subscript of some identifier we mean last part of it that is composed only from (decimal) digits and by root of some identifier we mean the whole identifier except for the subscript.

E.g. if we take foo42, then 42 is the subscript, and foo is the root.

Sourceval next_ident_away_in_goal : Environ.env -> Names.Id.t -> Names.Id.Set.t -> Names.Id.t

Avoid clashing with a name already used in current module

Sourceval next_global_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t

Avoid clashing with a name already used in current module but tolerate overwriting section variables, as in goals

Sourceval next_name_away : Names.Name.t -> Names.Id.Set.t -> Names.Id.t

Default is default_non_dependent_ident

Sourceval next_name_away_with_default : string -> Names.Name.t -> Names.Id.Set.t -> Names.Id.t
Sourceval next_name_away_with_default_using_types : string -> Names.Name.t -> Names.Id.Set.t -> EConstr.types -> Names.Id.t
Sourceval set_reserved_typed_name : (EConstr.types -> Names.Name.t) -> unit
Sourcetype renaming_flags =
  1. | RenamingForCasesPattern of Names.Name.t list * EConstr.constr
    (*

    avoid only global constructors

    *)
  2. | RenamingForGoal
    (*

    avoid all globals (as in intro)

    *)
  3. | RenamingElsewhereFor of Names.Name.t list * EConstr.constr
Sourceval make_all_rel_context_name_different : Environ.env -> Evd.evar_map -> EConstr.rel_context -> Environ.env * EConstr.rel_context
Sourceval make_all_name_different : Environ.env -> Evd.evar_map -> Environ.env
Sourceval compute_displayed_name_in_gen : (Evd.evar_map -> int -> 'a -> bool) -> Environ.env -> Evd.evar_map -> Names.Id.Set.t -> Names.Name.t -> 'a -> Names.Name.t * Names.Id.Set.t