package coq

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Libraries
1. coq.lib
2. coq.vm
3. coq.kernel
4. coq.library
5. coq.engine
6. coq.pretyping
7. coq.interp
8. coq.grammar
9. coq.proofs
10. coq.parsing
11. coq.printing
12. coq.tactics
13. coq.vernac
14. coq.stm
15. coq.toplevel
16. coq.highparsing
17. coq.idetop
18. coq.ide
19. coq.ltac

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.ide
coq.idetop
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.lib
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.ltac
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
coq.vm

Legend:
Library
Module
Module type
Parameter
Class
Class type

coq 8.7.2

Libraries

This package provides the following libraries (via ocamlobjinfo):

coq.lib

Documentation:

coq.vm

Documentation:

coq.kernel

Documentation:

coq.library

Documentation:

coq.engine

Documentation:

coq.pretyping

Documentation:

coq.interp

Documentation:

coq.grammar

Documentation:

Q_util
Argextend
Tacextend
Vernacextend

coq.proofs

Documentation:

coq.parsing

Documentation:

coq.printing

Documentation:

coq.tactics

Documentation:

coq.vernac

Documentation:

coq.stm

Documentation:

coq.toplevel

Documentation:

coq.highparsing

Documentation:

coq.idetop

Documentation:

coq.ide

Documentation:

coq.ltac

Documentation: