package coq

You can search for identifiers within the package.

in-package search v0.2.0

package coq

coq.clib
- Backtrace
- 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
- CStack
- 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
- Declare
- Discharge
- Dumpglob
- Genintern
  - Store
- Impargs
- Implicit_quantifiers
- Modintern
- Notation
  - NotationMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - NotationSet
- Notation_ops
- Notation_term
- NumTok
- 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
- Esubst
- Evar
  - Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Set
- IndTyping
- Indtypes
- Inductive
- Mod_subst
- Mod_typing
- Modops
- Names
  - Cmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Cmap_env
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Constant
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Constrmap
  - Constrmap_env
  - Cpred
  - Cset
  - Cset_env
  - 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
  - Indmap_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
  - 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
- Retroknowledge
- Retypeops
- Safe_typing
- Sorts
  - List
- Subtyping
- Term
- Term_typing
- TransparentState
- Type_errors
- Typeops
- UGraph
- Uint63
- Univ
  - AUContext
  - Constraint
  - ContextSet
  - Instance
  - LMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - LSet
  - Level
    
    UGlobal
  - UContext
  - Universe
  - 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
- 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
  - Stack
  - String
    
    List
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Set
  - Union
coq.library
- Coqlib
- Decl_kinds
- Declaremods
- Decls
- Global
- Globnames
  - ExtRefOrdered
- Goptions
  - MakeRefTable
    
    A
  - MakeStringTable
    
    A
  - OptionMap
- Keys
- Kindops
- Lib
- Libnames
  - Dirmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Dirset
  - Spmap
- Libobject
- Library
- Loadpath
- 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
  - LexerDiff
- Extend
- G_constr
- G_prim
- Notation_gram
- Notgram_ops
- Pcoq
  - Constr
  - Entry
  - GramState
  - Module
  - Parsable
  - Prim
- Ppextend
- Tok
coq.pretyping
- Arguments_renaming
- Cases
- Cbv
- Classops
- Coercion
- Constr_matching
- Detyping
  - PrintingInductiveMake
    
    Test
- Evarconv
- Evardefine
- Evarsolve
- Find_subterm
- Geninterp
  - TacStore
  - Val
  - ValTMap
    
    Value
- GlobEnv
- Glob_ops
- Glob_term
- Heads
- Indrec
- Inductiveops
- InferCumulativity
- 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
- Prettyp
- Printer
  - ContextObjectMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - ContextObjectSet
- Printmod
- Proof_diffs
  - StringMap
coq.proofs
- Clenv
- Clenvtac
- Evar_refiner
- Goal
  - Set
  - V82
- Goal_select
- Logic
- Miscprint
- Pfedit
- Proof
  - V82
- Proof_bullet
- Proof_global
- 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
- 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
- Leminv
- 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
- Class
- Classes
- ComAssumption
- ComDefinition
- ComFixpoint
- ComInductive
- ComProgramFixpoint
- DeclareDef
- Egramcoq
- Egramml
- ExplainErr
- G_proofs
- G_vernac
- Himsg
- Indschemes
- Lemmas
- Locality
- Metasyntax
- Mltop
- Obligations
- Ppvernac
- Proof_using
- Pvernac
  - Unsafe
  - Vernac_
- Record
- Search
- Topfmt
- Vernacentries
- Vernacexpr
- Vernacextend
- Vernacprop
- Vernacstate
  - Parser
  - Proof_global

Legend:
Library
Module
Module type
Parameter
Class
Class type

type tactic = Proofview.V82.tac

val sig_it : 'a Evd.sigma -> 'a

val project : Goal.goal Evd.sigma -> Evd.evar_map

val re_sig : 'a -> Evd.evar_map -> 'a Evd.sigma

val pf_concl : Goal.goal Evd.sigma -> EConstr.types

val pf_env : Goal.goal Evd.sigma -> Environ.env

val pf_hyps : Goal.goal Evd.sigma -> EConstr.named_context

val pf_hyps_types : 
  Goal.goal Evd.sigma ->
  (Names.Id.t Context.binder_annot * EConstr.types) list

val pf_nth_hyp_id : Goal.goal Evd.sigma -> int -> Names.Id.t

val pf_last_hyp : Goal.goal Evd.sigma -> EConstr.named_declaration

val pf_ids_of_hyps : Goal.goal Evd.sigma -> Names.Id.t list

val pf_global : 
  Goal.goal Evd.sigma ->
  Names.Id.t ->
  Evd.evar_map * EConstr.constr

val pf_unsafe_type_of : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.types

val pf_type_of : 
  Goal.goal Evd.sigma ->
  EConstr.constr ->
  Evd.evar_map * EConstr.types

val pf_hnf_type_of : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.types

val pf_get_hyp : Goal.goal Evd.sigma -> Names.Id.t -> EConstr.named_declaration

val pf_get_hyp_typ : Goal.goal Evd.sigma -> Names.Id.t -> EConstr.types

val pf_get_new_id : Names.Id.t -> Goal.goal Evd.sigma -> Names.Id.t

val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Goal.goal Evd.sigma -> 'a

val pf_eapply : 
  (Environ.env -> Evd.evar_map -> 'a -> Evd.evar_map * 'b) ->
  Goal.goal Evd.sigma ->
  'a ->
  Goal.goal Evd.sigma * 'b

val pf_reduce : 
  (Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr) ->
  Goal.goal Evd.sigma ->
  EConstr.constr ->
  EConstr.constr

val pf_e_reduce : 
  (Environ.env ->
    Evd.evar_map ->
    EConstr.constr ->
    Evd.evar_map * EConstr.constr) ->
  Goal.goal Evd.sigma ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

val pf_whd_all : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr

val pf_hnf_constr : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr

val pf_nf : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr

val pf_nf_betaiota : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr

val pf_reduce_to_quantified_ind : 
  Goal.goal Evd.sigma ->
  EConstr.types ->
  (Names.inductive * EConstr.EInstance.t) * EConstr.types

val pf_reduce_to_atomic_ind : 
  Goal.goal Evd.sigma ->
  EConstr.types ->
  (Names.inductive * EConstr.EInstance.t) * EConstr.types

val pf_compute : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr

val pf_unfoldn : 
  (Locus.occurrences * Names.evaluable_global_reference) list ->
  Goal.goal Evd.sigma ->
  EConstr.constr ->
  EConstr.constr

val pf_const_value : Goal.goal Evd.sigma -> Constr.pconstant -> EConstr.constr

val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool

val pf_conv_x_leq : 
  Goal.goal Evd.sigma ->
  EConstr.constr ->
  EConstr.constr ->
  bool

val pr_gls : Goal.goal Evd.sigma -> Pp.t

val pr_glls : Goal.goal list Evd.sigma -> Pp.t

deprecated Please move to "new" proof engine

module New : sig ... end