package coq

You can search for identifiers within the package.

in-package search v0.2.0

package coq

coq.engine
- EConstr
  - EInstance
  - ESorts
  - Unsafe
  - Vars
- Evarutil
- Evd
  - Filter
  - Metamap
    
    Monad
    
    M
    
    Unsafe
  - Metaset
  - Monad
    
    List
  - MonadR
    
    List
  - Store
- Ftactic
  - List
  - Notations
- Geninterp
  - TacStore
  - Val
- Logic_monad
  - BackState
  - Logical
    
    List
    
    P
    
    Unsafe
  - NonLogical
    
    List
  - Param
- Namegen
- Proofview
  - Goal
  - Monad
    
    List
  - NonLogical
    
    List
  - Notations
  - Trace
  - Unsafe
  - UnsafeRepr
  - V82
- Proofview_monad
  - Comb
  - Env
  - Giveup
  - Info
  - InfoL
  - Logical
    
    List
    
    Unsafe
  - P
  - Pv
  - Shelf
  - Solution
  - State
  - Status
  - Trace
  - Writer
- Termops
- UState
- Universes
  - Constraints
  - UF
coq.grammar
- Q_util
coq.highparsing
- G_constr
- G_prim
- G_proofs
- G_vernac
coq.interp
- Constrexpr_ops
- Constrextern
- Constrintern
- Declare
- Discharge
- Dumpglob
- Genintern
  - Store
- Impargs
- Implicit_quantifiers
- Modintern
- Notation
- Notation_ops
- Ppextend
- Reserve
- Smartlocate
- Stdarg
- Syntax_def
- Topconstr
coq.kernel
- CClosure
  - RedFlags
  - RedFlagsSig
- Cbytecodes
  - FvMap
  - Label
- Cbytegen
- Cemitcodes
- Constr
- Context
  - Compacted
    
    Declaration
  - Named
    
    Declaration
  - Rel
    
    Declaration
- Conv_oracle
- Cooking
- Copcodes
- Csymtable
- Declarations
- Declareops
- Environ
- Esubst
- Evar
  - Map
    
    Monad
    
    M
    
    Unsafe
  - Set
- Indtypes
- Inductive
- Mod_subst
- Mod_typing
- Modops
- Names
  - Cmap
    
    Monad
    
    M
    
    Unsafe
  - Cmap_env
    
    Monad
    
    M
    
    Unsafe
  - Constant
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Constrmap
  - Constrmap_env
  - Cpred
  - Cset
  - Cset_env
  - DirPath
  - Id
    
    List
    
    Map
    
    Monad
    
    M
    
    Unsafe
    
    Pred
    
    Set
  - Idmap
    
    Monad
    
    M
    
    Unsafe
  - Idpred
  - Idset
  - Indmap
  - Indmap_env
  - KNmap
    
    Monad
    
    M
    
    Unsafe
  - KNpred
  - KNset
  - KerName
  - Label
    
    Map
    
    Monad
    
    M
    
    Unsafe
    
    Set
  - MBId
  - MBImap
    
    Monad
    
    M
    
    Unsafe
  - MBIset
  - MPmap
    
    Monad
    
    M
    
    Unsafe
  - MPset
  - Mindmap
    
    Monad
    
    M
    
    Unsafe
  - Mindmap_env
  - Mindset
  - ModIdmap
    
    Monad
    
    M
    
    Unsafe
  - ModIdset
  - ModPath
  - MutInd
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Name
  - Projection
    
    SyntacticOrd
- Nativecode
- Nativeconv
- Nativelambda
- Nativelib
- Nativelibrary
- Nativevalues
- Opaqueproof
- Pre_env
- Primitives
- Reduction
- Retroknowledge
- Safe_typing
- Sorts
  - List
- Subtyping
- Term
- Term_typing
- Type_errors
- Typeops
- UGraph
- Uint31
- Univ
  - ACumulativityInfo
  - AUContext
  - Constraint
  - ContextSet
  - CumulativityInfo
  - Instance
  - LMap
    
    Monad
    
    M
    
    Unsafe
  - LSet
  - Level
  - UContext
  - Universe
- Vars
- Vconv
- Vm
coq.library
- Coqlib
- Declaremods
- Decls
- Dischargedhypsmap
- Global
- Globnames
  - ExtRefOrdered
  - RefOrdered
  - RefOrdered_env
  - Refmap
    
    Monad
    
    M
    
    Unsafe
  - Refmap_env
    
    Monad
    
    M
    
    Unsafe
  - Refset
  - Refset_env
- Goptions
  - MakeRefTable
    
    A
  - MakeStringTable
    
    A
  - OptionMap
- Heads
- Keys
- Kindops
- Lib
- Libnames
  - Dirmap
    
    Monad
    
    M
    
    Unsafe
  - Dirset
  - Spmap
- Libobject
- Library
- Loadpath
- Nameops
  - Name
- Nametab
  - EqualityType
  - Make
    
    E
    
    U
  - NAMETREE
  - UserName
- States
- Summary
  - Local
- Univops
coq.parsing
- CLexer
  - Error
- Egramcoq
- Egramml
- Pcoq
  - Constr
  - Gram
    
    Entry
    
    Unsafe
  - GramState
  - Module
  - Prim
  - Vernac_
- Tok
coq.pretyping
- Arguments_renaming
- Cases
- Cbv
- Classops
- Coercion
- Constr_matching
- Detyping
  - PrintingInductiveMake
    
    Test
- Evarconv
- Evardefine
- Evarsolve
- Find_subterm
- Glob_ops
- Indrec
- Inductiveops
- Locusops
- Miscops
- Nativenorm
- Patternops
- Pretype_errors
- Pretyping
- Program
- Recordops
- Redops
- Reductionops
- Retyping
- Tacred
- Typeclasses
- Typeclasses_errors
- Typing
- Unification
- Vnorm
coq.printing
- Genprint
- Ppconstr
- Pputils
- Ppvernac
- Prettyp
- Printer
  - ContextObjectMap
    
    Monad
    
    M
    
    Unsafe
  - ContextObjectSet
- Printmod
coq.proofs
- Clenv
- Clenvtac
- Evar_refiner
- Goal
  - V82
- Logic
- Miscprint
- Pfedit
- Proof
  - V82
- Proof_global
  - Bullet
  - V82
- Proof_using
- Redexpr
- Refine
- Refiner
- Tacmach
  - New
coq.stm
- AsyncTaskQueue
  - MakeQueue
    
    T
  - MakeWorker
    
    T
  - Task
- CoqworkmgrApi
- Dag
  - Make
    
    NodeSet
    
    OT
    
    Property
  - S
    
    NodeSet
    
    Property
- ProofBlockDelimiter
- Spawned
- Stm
  - DynBlockData
    
    Easy
    
    Map
    
    M
  - ProofTask
  - QueryTask
  - TacTask
- TQueue
- Vcs
  - Make
    
    Branch
    
    Dag
    
    NodeSet
    
    Property
    
    OT
  - S
    
    Branch
    
    Dag
    
    NodeSet
    
    Property
- Vernac_classifier
- Vio_checking
- WorkerLoop
- WorkerPool
  - Make
    
    Model
  - PoolModel
coq.tactics
- Auto
- Autorewrite
- Btermdn
  - Make
    
    Z
- Class_tactics
  - Search
- Contradiction
- Dn
  - Make
    
    Y
    
    Z
- Dnet
  - Datatype
  - Make
    
    Ident
    
    Idset
    
    Meta
    
    T
  - S
    
    Idset
- Eauto
- Elim
- Elimschemes
- Eqdecide
- Eqschemes
- Equality
- Hints
  - Hint_db
- Hipattern
- Ind_tables
- Inv
- Leminv
- Tacticals
  - New
- Tactics
  - New
  - Simple
- Term_dnet
  - IDENT
  - Make
    
    Ident
    
    Opt
  - OPT
  - S
coq.toplevel
- Coqinit
- Coqloop
- Coqtop
- Usage
- Vernac
coq.vernac
- Assumptions
- Auto_ind_decl
- Class
- Classes
- Command
- DeclareDef
- ExplainErr
- Himsg
- Indschemes
- Lemmas
- Locality
  - LocalityFixme
- Metasyntax
- Mltop
- Obligations
- Record
- Search
- Topfmt
- Vernacentries
- Vernacinterp
- Vernacprop

Legend:
Library
Module
Module type
Parameter
Class
Class type

type vodigest =

| Dvo_or_vi of Digest.t
| Dvivo of Digest.t * Digest.t

val digest_match : actual:vodigest -> required:vodigest -> bool

type safe_environment

val empty_environment : safe_environment

val is_initial : safe_environment -> bool

val env_of_safe_env : safe_environment -> Environ.env

type safe_transformer0 = safe_environment -> safe_environment

type !'a safe_transformer = safe_environment -> 'a * safe_environment

type private_constant

type private_constants

type private_constant_role =

| Subproof
| Schema of Names.inductive * string

val side_effects_of_private_constants : 
  private_constants ->
  Entries.side_effect list

val empty_private_constants : private_constants

val add_private : private_constant -> private_constants -> private_constants

val concat_private : 
  private_constants ->
  private_constants ->
  private_constants

val private_con_of_con : safe_environment -> Names.constant -> private_constant

val private_con_of_scheme : 
  kind:string ->
  safe_environment ->
  (Names.inductive * Names.constant) list ->
  private_constant

val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output

val inline_private_constants_in_constr : 
  Environ.env ->
  Constr.constr ->
  private_constants ->
  Constr.constr

val inline_private_constants_in_definition_entry : 
  Environ.env ->
  private_constants Entries.definition_entry ->
  private_constants Entries.definition_entry

val universes_of_private : private_constants -> Univ.universe_context_set list

val is_curmod_library : safe_environment -> bool

val join_safe_environment : 
  ?except:Future.UUIDSet.t ->
  safe_environment ->
  safe_environment

val is_joined_environment : safe_environment -> bool

val push_named_assum : 
  (Names.Id.t * Term.types * bool) Univ.in_universe_context_set ->
  safe_transformer0

val push_named_def : 
  (Names.Id.t * private_constants Entries.definition_entry) ->
  Univ.universe_context_set safe_transformer

type global_declaration =

| ConstantEntry of bool * private_constants Entries.constant_entry
| GlobalRecipe of Cooking.recipe

type exported_private_constant =
  Names.constant
  * private_constants Entries.constant_entry
  * private_constant_role

val add_constant : 
  Names.DirPath.t ->
  Names.Label.t ->
  global_declaration ->
  (Names.constant * exported_private_constant list) safe_transformer

val add_mind : 
  Names.DirPath.t ->
  Names.Label.t ->
  Entries.mutual_inductive_entry ->
  Names.mutual_inductive safe_transformer

val add_module : 
  Names.Label.t ->
  Entries.module_entry ->
  Declarations.inline ->
  (Names.module_path * Mod_subst.delta_resolver) safe_transformer

val add_modtype : 
  Names.Label.t ->
  Entries.module_type_entry ->
  Declarations.inline ->
  Names.module_path safe_transformer

val push_context_set : bool -> Univ.universe_context_set -> safe_transformer0

val push_context : bool -> Univ.universe_context -> safe_transformer0

val add_constraints : Univ.constraints -> safe_transformer0

val set_engagement : Declarations.engagement -> safe_transformer0

val set_typing_flags : Declarations.typing_flags -> safe_transformer0

val start_module : Names.Label.t -> Names.module_path safe_transformer

val start_modtype : Names.Label.t -> Names.module_path safe_transformer

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

val end_module : 
  Names.Label.t ->
  (Entries.module_struct_entry * Declarations.inline) option ->
  (Names.module_path * Names.MBId.t list * Mod_subst.delta_resolver)
    safe_transformer

val end_modtype : 
  Names.Label.t ->
  (Names.module_path * Names.MBId.t list) safe_transformer

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

val current_modpath : safe_environment -> Names.module_path

val current_dirpath : safe_environment -> Names.dir_path

type compiled_library

type native_library = Nativecode.global list

val get_library_native_symbols : 
  safe_environment ->
  Names.DirPath.t ->
  Nativecode.symbols

val start_library : Names.DirPath.t -> Names.module_path safe_transformer

val export : 
  ?except:Future.UUIDSet.t ->
  safe_environment ->
  Names.DirPath.t ->
  Names.module_path * compiled_library * native_library

val import : 
  compiled_library ->
  Univ.universe_context_set ->
  vodigest ->
  Names.module_path safe_transformer

type judgment

val j_val : judgment -> Term.constr

val j_type : judgment -> Term.constr

val typing : safe_environment -> Term.constr -> judgment

val exists_objlabel : Names.Label.t -> safe_environment -> bool

val delta_of_senv : 
  safe_environment ->
  Mod_subst.delta_resolver * Mod_subst.delta_resolver

val retroknowledge : 
  (Retroknowledge.retroknowledge -> 'a) ->
  safe_environment ->
  'a

val register : 
  Retroknowledge.field ->
  Retroknowledge.entry ->
  Term.constr ->
  safe_transformer0

val register_inline : Names.constant -> safe_transformer0

val set_strategy : 
  safe_environment ->
  Names.constant Names.tableKey ->
  Conv_oracle.level ->
  safe_environment