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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct