package coq

You can search for identifiers within the package.

in-package search v0.2.0

package coq

coq.clib
- Bigint
- CArray
  - ExtS
    
    Floatarray
    
    Fun1
    
    Smart
    
    Smart
  - Floatarray
  - Fun1
    
    Smart
  - S
    
    Floatarray
  - Smart
- CEphemeron
- CList
  - ExtS
    
    MonoS
    
    Smart
  - MonoS
  - S
  - Smart
- CMap
  - ExtS
    
    Monad
    
    M
    
    Set
    
    Smart
    
    Unsafe
  - Make
    
    M
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - MonadS
  - OrderedType
- CObj
- CSet
  - Hashcons
    
    H
    
    M
  - HashedType
  - Make
    
    M
  - OrderedType
- CString
  - ExtS
    
    List
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Set
  - List
  - Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - S
  - Set
- CThread
- CUnix
- Diff2
  - Make
    
    M
  - S
  - SeqType
- Dyn
  - Make
    
    Easy
    
    Map
    
    Value
  - MapS
  - S
    
    Easy
    
    Map
    
    Value
  - ValueS
- Exninfo
- HMap
  - HashedType
  - Make
    
    M
    
    Monad
    
    M
    
    Set
    
    Smart
    
    Unsafe
- Hashcons
  - HashconsedType
  - HashedType
  - Hlist
    
    D
  - Hstring
  - Make
    
    X
  - S
- Hashset
  - Combine
  - EqType
  - Make
    
    E
  - S
- Heap
  - Functional
    
    X
  - Ordered
  - S
- IStream
- Int
  - List
  - Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - PArray
  - PMap
  - Set
- Minisys
- Monad
  - Def
  - ListS
  - Make
    
    List
    
    M
  - S
    
    List
- Option
  - List
  - Smart
- OrderedType
  - Pair
    
    M
    
    N
  - S
  - UnorderedPair
    
    M
- Predicate
  - Make
    
    Ord
  - OrderedType
  - S
- Range
- Segmenttree
- Store
  - Make
  - S
- Terminal
- Trie
  - Grp
  - Make
    
    Data
    
    Label
  - S
- Unicode
- Unicodetable
- Unionfind
  - Make
    
    M
    
    S
  - MapS
  - PartitionSig
  - SetS
coq.config
- Coq_config
coq.engine
- EConstr
  - EInstance
  - ESorts
  - Unsafe
  - Vars
- Evar_kinds
- Evarutil
- Evd
  - Abstraction
  - Filter
  - Metamap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Metaset
  - MiniEConstr
    
    EInstance
    
    ESorts
  - Monad
    
    List
  - MonadR
    
    List
  - Store
- Ftactic
  - List
  - Notations
- Logic_monad
  - BackState
  - Logical
    
    List
    
    P
    
    Unsafe
  - NonLogical
    
    List
  - Param
- Namegen
- Nameops
  - Name
  - Subscript
- Proofview
  - Goal
  - Monad
    
    List
  - NonLogical
    
    List
  - Notations
  - Progress
  - Trace
  - Unsafe
  - UnsafeRepr
  - V82
- Proofview_monad
  - Comb
  - Env
  - Giveup
  - Info
  - InfoL
  - Logical
    
    List
    
    Unsafe
  - P
  - Pv
  - Shelf
  - Solution
  - State
  - StateStore
  - Status
  - Trace
  - Writer
- Termops
  - Internal
- UState
- UnivGen
- UnivMinim
  - UPairSet
- UnivNames
- UnivProblem
  - Set
- UnivSubst
- Univops
coq.interp
- Constrexpr
- Constrexpr_ops
- Constrextern
- Constrintern
- Decls
- Deprecation
- Dumpglob
- Genintern
  - Store
- Impargs
- Implicit_quantifiers
- Modintern
- Notation
  - NotationMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - NotationSet
  - SpecificNotationMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - SpecificNotationSet
- Notation_ops
- Notation_term
- NumTok
  - Signed
  - SignedNat
  - Unsigned
  - UnsignedNat
- Reserve
- Smartlocate
- Stdarg
- Syntax_def
- Tactypes
coq.kernel
- CClosure
- CPrimitives
- Cbytecodes
  - Label
- Cbytegen
- Cemitcodes
- Clambda
- Constr
- Context
  - Compacted
    
    Declaration
  - Named
    
    Declaration
  - Rel
    
    Declaration
- Conv_oracle
- Cooking
- Copcodes
- Csymtable
- Declarations
- Declareops
- Entries
- Environ
  - Globals
- Esubst
- Evar
  - Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Set
- Float64
- IndTyping
- Indtypes
- Inductive
- InferCumulativity
- Mod_subst
- Mod_typing
- Modops
- Names
  - Cmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Cmap_env
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Constant
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Constrmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Constrmap_env
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Constrset
  - Constrset_env
  - Cpred
  - Cset
  - Cset_env
  - DPmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - DPset
  - DirPath
  - GlobRef
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Map_env
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Ordered
    
    Ordered_env
    
    Set
    
    Set_env
  - Id
    
    List
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Pred
    
    Set
  - Indmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Indmap_env
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Indset
  - Indset_env
  - KNmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - KNpred
  - KNset
  - KerName
  - Label
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Set
  - MBId
  - MBImap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - MBIset
  - MPmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - MPset
  - Mindmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Mindmap_env
    
    Monad
    
    M
    
    Set
    
    Smart
    
    Unsafe
  - Mindset
  - ModIdmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - ModIdset
  - ModPath
  - MutInd
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Name
  - Projection
    
    CanOrd
    
    Repr
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
    
    SyntacticOrd
- Nativecode
- Nativeconv
- Nativelambda
- Nativelib
- Nativelibrary
- Nativevalues
- Opaqueproof
- Primred
  - RedNative
    
    E
  - RedNativeEntries
- Reduction
- Relevanceops
- Retroknowledge
- Safe_typing
- Section
- Sorts
- Subtyping
- Term
- Term_typing
- TransparentState
- Type_errors
- Typeops
- UGraph
  - Bound
- Uint63
- Univ
  - AUContext
  - Constraint
  - ContextSet
  - Instance
  - LMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - LSet
  - Level
    
    UGlobal
  - UContext
  - Universe
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Set
  - Variance
- Vars
- Vconv
- Vm
- Vmvalues
coq.lib
- AcyclicGraph
  - Make
    
    Point
    
    Constraint
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Set
  - Point
    
    Constraint
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Set
- Aux_file
  - H
  - M
- CAst
- CErrors
- CProfile
- CWarnings
- Control
- CoqProject_file
- DAst
- Envars
- Explore
  - Make
    
    S
  - SearchProblem
- Feedback
- Flags
- Future
  - UUID
  - UUIDMap
  - UUIDSet
- Genarg
  - ArgT
  - GenObj
  - Register
    
    M
- Hook
- Loc
- ObjFile
- Pp
- Pp_diff
  - StringDiff
- RemoteCounter
- Rtree
  - Smart
- Spawn
  - Async
    
    ML
  - Control
  - MainLoopModel
  - Sync
- Stateid
  - Self
  - Set
- System
- Util
  - Array
    
    Floatarray
    
    Fun1
    
    Smart
    
    Smart
  - Empty
  - List
    
    MonoS
    
    Smart
  - Map
    
    ExtS
    
    Monad
    
    M
    
    Set
    
    Smart
    
    Unsafe
    
    Make
    
    M
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    MonadS
    
    OrderedType
  - Set
    
    Hashcons
    
    H
    
    M
    
    HashedType
    
    Make
    
    M
    
    OrderedType
  - String
    
    List
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Set
  - Union
coq.library
- Coqlib
- Global
- Globnames
  - ExtRefMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - ExtRefOrdered
  - ExtRefSet
- Goptions
  - MakeRefTable
    
    A
    
    Set
  - MakeStringTable
    
    A
  - OptionMap
- Lib
- Libnames
  - Spmap
- Libobject
  - Dyn
    
    Easy
    
    Map
    
    Value
- Nametab
  - EqualityType
  - GlobDirRef
  - Make
    
    E
    
    U
  - NAMETREE
  - UnivIdMap
    
    Monad
    
    M
    
    Set
    
    Smart
    
    Unsafe
  - UserName
- States
- Summary
  - Dyn
    
    Easy
    
    Map
    
    Value
  - Local
coq.parsing
- CLexer
  - Error
  - Lexer
    
    State
  - LexerDiff
    
    State
- Extend
- G_constr
- G_prim
- Notation_gram
- Notgram_ops
- Pcoq
  - Constr
  - Entry
  - GramState
  - Lookahead
  - Module
  - Parsable
  - Prim
  - Production
  - Rule
  - Rules
  - Symbol
- Ppextend
- Tok
coq.pretyping
- Arguments_renaming
- Cases
- Cbv
- Coercion
- Coercionops
- Constr_matching
- Detyping
  - PrintingInductiveMake
    
    Test
- Evarconv
- Evardefine
- Evarsolve
- Find_subterm
- Geninterp
  - TacStore
  - Val
  - ValTMap
    
    Value
- GlobEnv
- Glob_ops
- Glob_term
- Heads
- Indrec
- Inductiveops
- Keys
- Locus
- Locusops
- Ltac_pretype
- Nativenorm
- Pattern
- Patternops
- Pretype_errors
- Pretyping
- Program
- Recordops
- Reductionops
- Retyping
- Tacred
- Typeclasses
- Typeclasses_errors
- Typing
- Unification
- Vnorm
coq.printing
- Genprint
- Ppconstr
- Pputils
- Printer
  - ContextObjectMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - ContextObjectSet
- Printmod
- Proof_diffs
coq.proofs
- Clenv
- Clenvtac
- Evar_refiner
- Goal
  - Set
  - V82
- Goal_select
- Logic
- Miscprint
- Proof
  - V82
- Proof_bullet
- Refine
- Refiner
- Tacmach
  - New
coq.stm
- AsyncTaskQueue
  - MakeQueue
    
    T
  - MakeWorker
    
    T
  - Task
- CoqworkmgrApi
- Dag
  - Make
    
    NodeSet
    
    OT
    
    Property
  - S
    
    NodeSet
    
    Property
- ProofBlockDelimiter
- Spawned
- Stm
  - AsyncOpts
  - DynBlockData
    
    Easy
    
    Map
    
    Value
  - ProofTask
  - QueryTask
  - TacTask
- TQueue
- Vcs
  - Make
    
    Branch
    
    Dag
    
    NodeSet
    
    Property
    
    OT
  - S
    
    Branch
    
    Dag
    
    NodeSet
    
    Property
- Vernac_classifier
- Vio_checking
- WorkerPool
  - Make
    
    Model
  - PoolModel
coq.tactics
- Abstract
- Auto
- Autorewrite
- Btermdn
  - Make
    
    Z
- Class_tactics
  - Search
- Contradiction
- DeclareScheme
- DeclareUctx
- Dn
  - Make
    
    Y
    
    Z
- Dnet
  - Datatype
  - Make
    
    Ident
    
    Idset
    
    Meta
    
    T
  - S
    
    Idset
- Eauto
- Elim
- Elimschemes
- Eqdecide
- Eqschemes
- Equality
- Genredexpr
- Hints
  - Hint_db
- Hipattern
- Ind_tables
- Inv
- Ppred
- Redexpr
- Redops
- Tacticals
  - New
- Tactics
  - New
  - Simple
- Term_dnet
  - IDENT
  - Make
    
    Ident
    
    Opt
  - OPT
  - S
coq.toplevel
- Ccompile
- Coqargs
- Coqc
- Coqcargs
- Coqinit
- Coqloop
- Coqtop
- G_toplevel
  - Toplevel_
- Usage
- Vernac
  - State
- WorkerLoop
coq.vernac
- Assumptions
- Attributes
  - Notations
- Auto_ind_decl
- Canonical
- Classes
- ComArguments
- ComAssumption
- ComCoercion
- ComDefinition
- ComFixpoint
- ComHints
- ComInductive
- ComPrimitive
- ComProgramFixpoint
- ComSearch
- Declare
  - Hook
    
    S
  - Internal
    
    Constant
  - Proof
  - Recthm
- DeclareDef
- DeclareInd
  - Internal
- DeclareObl
  - Obligation
  - ProgMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - ProgramDecl
- DeclareUniv
- Declaremods
- Egramcoq
- Egramml
- G_proofs
- G_vernac
- Himsg
- Indschemes
- Lemmas
- Library
- Loadpath
- Locality
- Metasyntax
- Mltop
- Obligations
- Pfedit
- Ppvernac
- Prettyp
- Proof_global
- Proof_using
- Pvernac
  - Unsafe
  - Vernac_
- RecLemmas
- Record
- RetrieveObl
- Search
- Topfmt
- Vernacentries
- Vernacexpr
- Vernacextend
- Vernacinterp
- Vernacprop
- Vernacstate

Legend:
Library
Module
Module type
Parameter
Class
Class type

exception EqNotFound of Names.inductive * Names.inductive

exception EqUnknown of string

exception UndefinedCst of string

exception InductiveWithProduct

exception InductiveWithSort

exception ParameterWithoutEquality of Names.GlobRef.t

exception NonSingletonProp of Names.inductive

exception DecidabilityMutualNotSupported

exception NoDecidabilityCoInductive

exception ConstructorWithNonParametricInductiveType of Names.inductive

exception DecidabilityIndicesNotSupported

val beq_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind

val build_beq_scheme : Ind_tables.mutual_scheme_object_function

val lb_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind

val make_lb_scheme : Ind_tables.mutual_scheme_object_function

val bl_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind

val make_bl_scheme : Ind_tables.mutual_scheme_object_function

val eq_dec_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind

val make_eq_decidability : Ind_tables.mutual_scheme_object_function