package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val new_meta : unit -> Term.metavariable
val mk_new_meta : unit -> EConstr.constr
val new_evar : Environ.env -> Evd.evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?candidates:EConstr.constr list -> ?store:Evd.Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> EConstr.types -> Evd.evar_map * EConstr.t
val new_pure_evar : Environ.named_context_val -> Evd.evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?candidates:EConstr.constr list -> ?store:Evd.Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> EConstr.types -> Evd.evar_map * Evd.evar
val new_pure_evar_full : Evd.evar_map -> Evd.evar_info -> Evd.evar_map * Evd.evar
val e_new_evar : Environ.env -> Evd.evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?candidates:EConstr.constr list -> ?store:Evd.Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> EConstr.types -> EConstr.constr
val new_type_evar : Environ.env -> Evd.evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> Evd.rigid -> Evd.evar_map * (EConstr.constr * Term.sorts)
val e_new_type_evar : Environ.env -> Evd.evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> Evd.rigid -> EConstr.constr * Term.sorts
val e_new_Type : ?rigid:Evd.rigid -> Environ.env -> Evd.evar_map ref -> EConstr.constr
val new_evar_instance : Environ.named_context_val -> Evd.evar_map -> EConstr.types -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?candidates:EConstr.constr list -> ?store:Evd.Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> EConstr.constr list -> Evd.evar_map * EConstr.constr
val make_pure_subst : Evd.evar_info -> 'a array -> (Names.Id.t * 'a) list
val safe_evar_value : Evd.evar_map -> Constr.existential -> Constr.constr option
val non_instantiated : Evd.evar_map -> Evd.evar_info Evar.Map.t
exception NoHeadEvar
val whd_head_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
val has_undefined_evars : Evd.evar_map -> EConstr.constr -> bool
val is_ground_term : Evd.evar_map -> EConstr.constr -> bool
val is_ground_env : Evd.evar_map -> Environ.env -> bool
val gather_dependent_evars : Evd.evar_map -> Evd.evar list -> Evar.Set.t option Evar.Map.t
val advance : Evd.evar_map -> Evd.evar -> Evd.evar option
val undefined_evars_of_term : Evd.evar_map -> EConstr.constr -> Evar.Set.t
val undefined_evars_of_named_context : Evd.evar_map -> Context.Named.t -> Evar.Set.t
val undefined_evars_of_evar_info : Evd.evar_map -> Evd.evar_info -> Evar.Set.t
val occur_evar_upto : Evd.evar_map -> Evar.t -> EConstr.constr -> bool
val nf_named_context_evar : Evd.evar_map -> Context.Named.t -> Context.Named.t
val nf_rel_context_evar : Evd.evar_map -> EConstr.rel_context -> EConstr.rel_context
val nf_env_evar : Evd.evar_map -> Environ.env -> Environ.env
val nf_evar_info : Evd.evar_map -> Evd.evar_info -> Evd.evar_info
val nf_evar_map : Evd.evar_map -> Evd.evar_map
val nf_evar_map_undefined : Evd.evar_map -> Evd.evar_map
val nf_evars_universes : Evd.evar_map -> Constr.constr -> Constr.constr
val nf_evars_and_universes : Evd.evar_map -> Evd.evar_map * (Constr.constr -> Constr.constr)
val nf_evar_map_universes : Evd.evar_map -> Evd.evar_map * (Constr.constr -> Constr.constr)
exception Uninstantiated_evar of Term.existential_key
val flush_and_check_evars : Evd.evar_map -> EConstr.constr -> Constr.constr
val eq_constr_univs_test : Evd.evar_map -> Evd.evar_map -> Constr.constr -> Constr.constr -> bool
type clear_dependency_error =
  1. | OccurHypInSimpleClause of Names.Id.t option
  2. | EvarTypingBreak of Constr.existential
exception ClearDependencyError of Names.Id.t * clear_dependency_error
type csubst
val empty_csubst : csubst
val csubst_subst : csubst -> EConstr.constr -> EConstr.constr
type ext_named_context = csubst * (Names.Id.t * EConstr.constr) list * Names.Id.Set.t * EConstr.named_context
val push_rel_decl_to_named_context : Evd.evar_map -> EConstr.rel_declaration -> ext_named_context -> ext_named_context
val generalize_evar_over_rels : Evd.evar_map -> EConstr.existential -> EConstr.types * EConstr.constr list
val evd_comb0 : (Evd.evar_map -> Evd.evar_map * 'a) -> Evd.evar_map ref -> 'a
val evd_comb1 : (Evd.evar_map -> 'b -> Evd.evar_map * 'a) -> Evd.evar_map ref -> 'b -> 'a
val evd_comb2 : (Evd.evar_map -> 'b -> 'c -> Evd.evar_map * 'a) -> Evd.evar_map ref -> 'b -> 'c -> 'a
val meta_counter_summary_name : string
type type_constraint = EConstr.types option
type val_constraint = EConstr.constr option
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