package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val new_meta : unit -> Constr.metavariable
val mk_new_meta : unit -> EConstr.constr
val new_evar_from_context : 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 * EConstr.t
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 * Evar.t
val new_pure_evar_full : Evd.evar_map -> Evd.evar_info -> Evd.evar_map * Evar.t
val e_new_evar : Environ.env -> Evd.evar_map Pervasives.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 * Sorts.t)
val restrict_evar : Evd.evar_map -> Evar.t -> Evd.Filter.t -> ?src:Evar_kinds.t Loc.located -> EConstr.constr list option -> Evd.evar_map * Evar.t
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 head_evar : Evd.evar_map -> EConstr.constr -> Evar.t
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 -> Evar.t list -> Evar.Set.t option Evar.Map.t
val advance : Evd.evar_map -> Evar.t -> Evar.t 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
type undefined_evars_cache
val create_undefined_evars_cache : unit -> undefined_evars_cache
val filtered_undefined_evars_of_evar_info : ?cache:undefined_evars_cache -> 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 Evar.t
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
val compare_constructor_instances : Evd.evar_map -> Univ.Instance.t -> Univ.Instance.t -> Evd.evar_map
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.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 push_rel_context_to_named_context : Environ.env -> Evd.evar_map -> EConstr.types -> Environ.named_context_val * EConstr.types * EConstr.constr list * csubst
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 Pervasives.ref -> 'a
val evd_comb1 : (Evd.evar_map -> 'b -> Evd.evar_map * 'a) -> Evd.evar_map Pervasives.ref -> 'b -> 'a
val evd_comb2 : (Evd.evar_map -> 'b -> 'c -> Evd.evar_map * 'a) -> Evd.evar_map Pervasives.ref -> 'b -> 'c -> 'a
val meta_counter_summary_tag : int Summary.Dyn.tag
type type_constraint = EConstr.types option
  • deprecated use the version in Evardefine
type val_constraint = EConstr.constr option
  • deprecated use the version in Evardefine
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