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