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 universes_lbound : unit -> UGraph.Bound.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_indices_matter : bool -> unit
val set_typing_flags : Declarations.typing_flags -> unit
val set_check_guarded : bool -> unit
val set_check_positive : bool -> unit
val set_check_universes : bool -> unit
val typing_flags : unit -> Declarations.typing_flags
val set_cumulative_sprop : bool -> unit
val is_cumulative_sprop : unit -> bool
val set_allow_sprop : bool -> unit
val sprop_allowed : unit -> bool
val push_named_assum : (Names.Id.t * Constr.types) -> unit
val push_named_def : (Names.Id.t * Entries.section_def_entry) -> unit
val push_section_context : (Names.Name.t array * Univ.UContext.t) -> unit
val add_constraints : Univ.Constraint.t -> unit
val push_context_set : strict:bool -> Univ.ContextSet.t -> unit
val open_section : unit -> unit
val close_section : Summary.frozen -> unit
val sections_are_opened : unit -> bool
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 : Opaqueproof.indirect_accessor -> Names.Constant.t -> (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option
val body_of_constant_body : Opaqueproof.indirect_accessor -> Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * unit Opaqueproof.delayed_universes * 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 get_template_polymorphic_variables : Names.GlobRef.t -> Univ.Level.t list
val is_type_in_type : Names.GlobRef.t -> bool
val register_inline : Names.Constant.t -> unit
val register_inductive : Names.inductive -> 'a CPrimitives.prim_ind -> unit
val set_strategy : Names.Constant.t Names.tableKey -> Conv_oracle.level -> unit
val set_share_reduction : bool -> unit
val set_VM : bool -> unit
val set_native_compiler : 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