package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val safe_env : unit -> Safe_typing.safe_environment
val env : unit -> Environ.env
val env_is_initial : unit -> bool
val universes : unit -> UGraph.t
val named_context_val : unit -> Environ.named_context_val
val named_context : unit -> Constr.named_context
val set_engagement : Declarations.engagement -> unit
val set_typing_flags : Declarations.typing_flags -> unit
val typing_flags : unit -> Declarations.typing_flags
val push_named_assum : (Names.Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
val push_named_def : (Names.Id.t * Entries.section_def_entry) -> unit
val add_constraints : Univ.Constraint.t -> unit
val push_context : bool -> Univ.UContext.t -> unit
val push_context_set : bool -> Univ.ContextSet.t -> unit
val start_module : Names.Id.t -> Names.ModPath.t
val start_modtype : Names.Id.t -> Names.ModPath.t
val end_modtype : Summary.frozen -> Names.Id.t -> Names.ModPath.t * Names.MBId.t list
val exists_objlabel : Names.Label.t -> bool
val constant_of_delta_kn : Names.KerName.t -> Names.Constant.t
val mind_of_delta_kn : Names.KerName.t -> Names.MutInd.t
val opaque_tables : unit -> Opaqueproof.opaquetab
val body_of_constant : Names.Constant.t -> (Constr.constr * Univ.AUContext.t) option
val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
val start_library : Names.DirPath.t -> Names.ModPath.t
val env_of_context : Environ.named_context_val -> Environ.env
val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
val is_joined_environment : unit -> bool
val is_polymorphic : Names.GlobRef.t -> bool
val is_template_polymorphic : Names.GlobRef.t -> bool
val is_type_in_type : Names.GlobRef.t -> bool
val constr_of_global_in_context : Environ.env -> Names.GlobRef.t -> Constr.types * Univ.AUContext.t
val type_of_global_in_context : Environ.env -> Names.GlobRef.t -> Constr.types * Univ.AUContext.t
val universes_of_global : Names.GlobRef.t -> Univ.AUContext.t
val register : Retroknowledge.field -> Constr.constr -> Constr.constr -> unit
val register_inline : Names.Constant.t -> unit
val set_strategy : Names.Constant.t Names.tableKey -> Conv_oracle.level -> unit
val set_reduction_sharing : bool -> unit
val current_modpath : unit -> Names.ModPath.t
val current_dirpath : unit -> Names.DirPath.t
val with_global : (Environ.env -> Names.DirPath.t -> 'a Univ.in_universe_context_set) -> 'a
val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag
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