package coq

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Enriching the global environment
Queries in the global environment
Compiled libraries
Misc
Retroknowledge
Oracle
Conversion settings

Formal proof management system

Install

dune-project

Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.16.1.tar.gz

sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

doc/coq-core.library/Global/index.html

Module `Global`Source

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 env_is_initial : unit -> bool

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_cumulative_sprop : bool -> unit

Sourceval is_cumulative_sprop : unit -> bool

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

val export_private_constants : 
  Safe_typing.private_constants ->
  Safe_typing.exported_private_constant list

val add_constant : 
  ?typing_flags:Declarations.typing_flags ->
  Names.Id.t ->
  Safe_typing.global_declaration ->
  Names.Constant.t

Sourceval fill_opaque : Safe_typing.opaque_certificate -> unit

val add_private_constant : 
  Names.Id.t ->
  Univ.ContextSet.t ->
  Safe_typing.side_effect_declaration ->
  Names.Constant.t * Safe_typing.private_constants

val add_mind : 
  ?typing_flags:Declarations.typing_flags ->
  Names.Id.t ->
  Entries.mutual_inductive_entry ->
  Names.MutInd.t

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

val add_module : 
  Names.Id.t ->
  Entries.module_entry ->
  Declarations.inline ->
  Names.ModPath.t * Mod_subst.delta_resolver

val add_modtype : 
  Names.Id.t ->
  Entries.module_type_entry ->
  Declarations.inline ->
  Names.ModPath.t

val add_include : 
  Entries.module_struct_entry ->
  bool ->
  Declarations.inline ->
  Mod_subst.delta_resolver

Sections

Sourceval open_section : unit -> unit

poly is true when the section should be universe polymorphic

Sourceval close_section : Summary.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

val end_module : 
  Summary.frozen ->
  Names.Id.t ->
  (Entries.module_struct_entry * Declarations.inline) option ->
  Names.ModPath.t * Names.MBId.t list * Mod_subst.delta_resolver

val end_modtype : 
  Summary.frozen ->
  Names.Id.t ->
  Names.ModPath.t * Names.MBId.t list

val add_module_parameter : 
  Names.MBId.t ->
  Entries.module_struct_entry ->
  Declarations.inline ->
  Mod_subst.delta_resolver

Queries in the global environment

Sourceval lookup_named : Names.variable -> Constr.named_declaration

Sourceval lookup_constant : Names.Constant.t -> Declarations.constant_body

val lookup_inductive : 
  Names.inductive ->
  Declarations.mutual_inductive_body * Declarations.one_inductive_body

val lookup_pinductive : 
  Constr.pinductive ->
  Declarations.mutual_inductive_body * Declarations.one_inductive_body

Sourceval lookup_mind : Names.MutInd.t -> Declarations.mutual_inductive_body

Sourceval lookup_module : Names.ModPath.t -> Declarations.module_body

Sourceval lookup_modtype : Names.ModPath.t -> Declarations.module_type_body

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 = {

access_proof : Opaqueproof.opaque -> (Constr.t * unit Opaqueproof.delayed_universes) option;

}

val force_proof : 
  indirect_accessor ->
  Opaqueproof.opaque ->
  Constr.t * unit Opaqueproof.delayed_universes

val 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.

val 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

val export : 
  output_native_objects:bool ->
  Names.DirPath.t ->
  Names.ModPath.t * Safe_typing.compiled_library * Nativelib.native_library

val import : 
  Safe_typing.compiled_library ->
  Univ.ContextSet.t ->
  Safe_typing.vodigest ->
  Names.ModPath.t

Misc

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

Sourceval env_of_context : Environ.named_context_val -> Environ.env

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

Sourceval set_strategy : Names.Constant.t Names.tableKey -> Conv_oracle.level -> unit

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

val with_global : 
  (Environ.env -> Names.DirPath.t -> 'a Univ.in_universe_context_set) ->
  'a

Sourceval global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag

On This Page

Enriching the global environment
Queries in the global environment
Compiled libraries
Misc
Retroknowledge
Oracle
Conversion settings