package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module GlobalSource

This module defines the global environment of Coq. The functions below are exactly the same as the ones in Safe_typing, operating on that global environment. add_* functions perform name verification, i.e. check that the name given as argument match those provided by Safe_typing.

Sourceval safe_env : unit -> Safe_typing.safe_environment
Sourceval env : unit -> Environ.env
Sourceval universes : unit -> UGraph.t
Sourceval universes_lbound : unit -> UGraph.Bound.t
Sourceval named_context_val : unit -> Environ.named_context_val
Sourceval named_context : unit -> Constr.named_context
Enriching the global environment
Sourceval set_impredicative_set : bool -> unit

Changing the (im)predicativity of the system

Sourceval set_indices_matter : bool -> unit
Sourceval set_typing_flags : Declarations.typing_flags -> unit
Sourceval set_check_guarded : bool -> unit
Sourceval set_check_positive : bool -> unit
Sourceval set_check_universes : bool -> unit
Sourceval typing_flags : unit -> Declarations.typing_flags
Sourceval set_allow_sprop : bool -> unit
Sourceval sprop_allowed : unit -> bool

Variables, Local definitions, constants, inductive types

Sourceval push_named_assum : (Names.Id.t * Constr.types) -> unit
Sourceval push_named_def : (Names.Id.t * Entries.section_def_entry) -> unit
Sourceval push_section_context : Univ.UContext.t -> unit
Sourceval fill_opaque : Safe_typing.opaque_certificate -> unit
Sourceval add_constraints : Univ.Constraints.t -> unit

Extra universe constraints

Sourceval push_context_set : strict:bool -> Univ.ContextSet.t -> unit

Non-interactive modules and module types

Sections

Sourceval open_section : unit -> unit

poly is true when the section should be universe polymorphic

Sourceval close_section : Summary.Interp.frozen -> unit

Close the section and reset the global state to the one at the time when the section what opened.

Sourceval sections_are_opened : unit -> bool

Interactive modules and module types

Sourceval start_module : Names.Id.t -> Names.ModPath.t
Sourceval start_modtype : Names.Id.t -> Names.ModPath.t
Queries in the global environment
Sourceval exists_objlabel : Names.Label.t -> bool
Sourceval constant_of_delta_kn : Names.KerName.t -> Names.Constant.t
Sourceval mind_of_delta_kn : Names.KerName.t -> Names.MutInd.t
Sourcetype indirect_accessor = {
  1. access_proof : Opaqueproof.opaque -> (Constr.t * unit Opaqueproof.delayed_universes) option;
}
Sourceval body_of_constant : indirect_accessor -> Names.Constant.t -> (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AbstractContext.t) option

Returns the body of the constant if it has any, and the polymorphic context it lives in. For monomorphic constant, the latter is empty, and for polymorphic constants, the term contains De Bruijn universe variables that need to be instantiated.

Sourceval body_of_constant_body : indirect_accessor -> Declarations.constant_body -> (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AbstractContext.t) option

Same as body_of_constant but on constant_body.

Compiled libraries
Sourceval start_library : Names.DirPath.t -> Names.ModPath.t
Misc

Function to get an environment from the constants part of the global * environment and a given context.

Sourceval is_joined_environment : unit -> bool
Sourceval is_polymorphic : Names.GlobRef.t -> bool
Sourceval is_template_polymorphic : Names.GlobRef.t -> bool
Sourceval get_template_polymorphic_variables : Names.GlobRef.t -> Univ.Level.t list
Sourceval is_type_in_type : Names.GlobRef.t -> bool
Retroknowledge
Sourceval register_inline : Names.Constant.t -> unit
Sourceval register_inductive : Names.inductive -> 'a CPrimitives.prim_ind -> unit
Oracle
Conversion settings
Sourceval set_share_reduction : bool -> unit
Sourceval set_VM : bool -> unit
Sourceval set_native_compiler : bool -> unit
Sourceval current_modpath : unit -> Names.ModPath.t
Sourceval current_dirpath : unit -> Names.DirPath.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