package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

coq-core.boot
- Boot
  - Env
    
    Path
  - Path
  - Usage
  - Util
coq-core.clib
- CArray
  - ExtS
    
    Floatarray
    
    Fun1
    
    Smart
    
    Smart
  - Floatarray
  - Fun1
    
    Smart
  - Smart
- CEphemeron
- CList
  - MonoS
  - Smart
- CMap
  - ExtS
    
    Monad
    
    M
    
    Set
    
    Smart
  - MonadS
  - OrderedType
- CObj
- CSet
  - Hashcons
    
    H
    
    M
  - HashedType
  - OrderedType
- CString
  - ExtS
    
    List
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Pred
  - List
  - Map
    
    Monad
    
    M
    
    Smart
  - Pred
- CThread
- CUnix
- Diff2
  - Make
    
    M
  - S
  - SeqType
- Dyn
  - Make
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
  - MapS
  - S
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
  - ValueS
- Exninfo
- HMap
  - HashedType
  - Make
    
    M
    
    Monad
    
    M
    
    Set
    
    Smart
- 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
  - PArray
  - PMap
- Monad
  - Def
  - ListS
  - Make
    
    List
    
    M
  - S
    
    List
- NeList
- Option
  - List
  - Smart
- OrderedType
  - Pair
    
    M
    
    N
  - S
  - UnorderedPair
    
    M
- PolyMap
  - Make
    
    Map
    
    V
    
    MapS
    
    OneTag
    
    Tag
  - Tag
  - ValueS
- Predicate
  - Make
    
    Ord
  - OrderedType
  - S
- Range
- SList
  - Skip
  - Smart
- Segmenttree
- Store
  - Make
  - S
- Terminal
- Trie
  - Grp
  - Make
    
    Data
  - S
- Unicode
- Unicodetable
- Unionfind
  - Make
    
    M
    
    S
  - MapS
  - PartitionSig
  - SetS
coq-core.config
- Coq_config
coq-core.coqworkmgrapi
- CoqworkmgrApi
coq-core.engine
- EConstr
  - EInstance
  - ESorts
  - Unsafe
  - UnsafeMonomorphic
  - Vars
- Evar_kinds
- Evarutil
  - VarSet
- Evd
  - Abstraction
  - Filter
  - FutureGoals
  - Metamap
    
    Monad
    
    M
    
    Smart
  - 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
- Proofview_monad
  - Comb
  - Env
  - Info
  - InfoL
  - Logical
    
    List
    
    Unsafe
  - P
  - Pv
  - Reader
  - Solution
  - State
  - StateStore
  - Status
  - Trace
  - Writer
- Termops
  - Internal
- UState
  - Internal
- UnivFlex
- UnivGen
- UnivMinim
- UnivNames
- UnivProblem
  - Set
- UnivSubst
coq-core.gramlib
- Gramlib
  - Gramext
  - Grammar
    
    ExtS
    
    EState
    
    Entry
    
    GState
    
    Parsable
    
    Production
    
    Rule
    
    Rules
    
    Symbol
    
    Unsafe
    
    GMake
    
    EState
    
    Entry
    
    GState
    
    L
    
    State
    
    Parsable
    
    Production
    
    Rule
    
    Rules
    
    Symbol
    
    Unsafe
    
    S
    
    Entry
    
    Parsable
    
    Production
    
    Rule
    
    Rules
    
    Symbol
  - LStream
  - Plexing
    
    S
    
    State
  - Stream
coq-core.interp
- Abbreviation
- Constrexpr_ops
- Constrextern
- Constrintern
- Decls
- Dumpglob
- Genintern
  - Store
- Impargs
- Implicit_quantifiers
- Modintern
- Notation
  - NotationMap
    
    Monad
    
    M
    
    Smart
  - SpecificNotationMap
    
    Monad
    
    M
    
    Smart
- Notation_ops
- Notationextern
- NumTok
  - Signed
  - SignedNat
  - Unsigned
  - UnsignedNat
- Reserve
- Smartlocate
- Stdarg
coq-core.kernel
- CClosure
- CPrimitives
- Constant_typing
- Constr
  - UnsafeMonomorphic
- Context
  - Compacted
    
    Declaration
  - Named
    
    Declaration
  - Rel
    
    Declaration
- Conv_oracle
- Conversion
- Cooking
- Declareops
- Discharge
- Environ
  - Globals
  - QConstant
  - QConstruct
  - QGlobRef
  - QInd
  - QMutInd
  - QNameS
  - QProjection
    
    Repr
- Esubst
  - Internal
- Evar
  - Map
    
    Monad
    
    M
    
    Smart
- Float64
- Float64_common
- Genlambda
  - Make
    
    Val
  - S
- IndTyping
- Indtypes
- Inductive
- InferCumulativity
- Mod_subst
- Mod_typing
- Modops
- Names
  - Cmap
    
    Monad
    
    M
    
    Smart
  - Cmap_env
    
    Monad
    
    M
    
    Smart
  - Constant
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Constrmap
    
    Monad
    
    M
    
    Smart
  - Constrmap_env
    
    Monad
    
    M
    
    Smart
  - Construct
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Cpred
  - Cset
  - Cset_env
  - DPmap
    
    Monad
    
    M
    
    Smart
  - DirPath
  - EqType
  - GlobRef
    
    CanOrd
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Map_env
    
    Monad
    
    M
    
    Smart
    
    Set
    
    Set_env
    
    SyntacticOrd
    
    UserOrd
  - Id
    
    List
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Pred
  - Ind
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Indmap
    
    Monad
    
    M
    
    Smart
  - Indmap_env
    
    Monad
    
    M
    
    Smart
  - KNmap
    
    Monad
    
    M
    
    Smart
  - KNpred
  - KNset
  - KerName
  - Label
    
    Map
    
    Monad
    
    M
    
    Smart
  - MBId
  - MBImap
    
    Monad
    
    M
    
    Smart
  - MPmap
    
    Monad
    
    M
    
    Smart
  - Mindmap
    
    Monad
    
    M
    
    Smart
  - Mindmap_env
    
    Monad
    
    M
    
    Set
    
    Smart
  - Mindset
  - ModIdmap
    
    Monad
    
    M
    
    Smart
  - ModPath
  - MutInd
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Name
  - Projection
    
    CanOrd
    
    Repr
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
    
    SyntacticOrd
    
    UserOrd
  - QNameS
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
- Nativecode
- Nativeconv
- Nativelambda
- Nativelib
- Nativelibrary
- Nativevalues
- Opaqueproof
  - HandleMap
- Parray
- Primred
  - RedNative
    
    E
  - RedNativeEntries
- RedFlags
- Reduction
- Relevanceops
- Retroknowledge
- Safe_typing
- Section
- Sorts
  - QConstraint
  - QConstraints
  - QUConstraints
  - QVar
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Set
  - Quality
    
    Constants
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Set
- Subtyping
- Term
- TransparentState
- Type_errors
- Typeops
- UGraph
  - Bound
- UVars
- Uint63
- Univ
  - Constraints
  - ContextSet
  - Level
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Set
  - UGlobal
  - Universe
    
    Map
    
    Monad
    
    M
    
    Smart
- Vars
- Vconv
- Vm
- Vmbytecodes
  - Label
- Vmbytegen
- Vmemitcodes
- Vmerrors
- Vmlambda
- Vmopcodes
- Vmsymtable
- Vmvalues
coq-core.lib
- AcyclicGraph
  - Make
    
    Point
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Set
  - Point
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Set
- Aux_file
- CAst
  - Smart
- CDebug
- CErrors
- CProfile
- CWarnings
  - CoreCategories
- Control
- CoqProject_file
- Core_plugins_findlib_compat
- DAst
- Deprecation
  - Version
- Envars
- Feedback
- Flags
- Hook
- Instr
- Loc
- NewProfile
  - MiniJson
- ObjFile
- Pp
- Pp_diff
  - StringDiff
- Rtree
  - Smart
- Spawn
  - Async
    
    ML
  - Control
  - MainLoopModel
  - Sync
- Stateid
- System
- Util
  - Array
    
    Floatarray
    
    Fun1
    
    Smart
    
    Smart
  - Compare
  - Empty
  - List
    
    MonoS
    
    Smart
  - Map
    
    ExtS
    
    Monad
    
    M
    
    Set
    
    Smart
    
    MonadS
    
    OrderedType
  - Set
    
    Hashcons
    
    H
    
    M
    
    HashedType
    
    OrderedType
  - Union
coq-core.library
- Coqlib
- Global
- Globnames
  - ExtRefMap
    
    Monad
    
    M
    
    Smart
  - ExtRefOrdered
  - ExtRefSet
- Goptions
  - MakeRefTable
    
    A
    
    Set
  - MakeStringTable
    
    A
  - OptionMap
- Lib
- Libnames
  - Spmap
- Libobject
  - Dyn
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
- Library_info
- Nametab
  - EqualityType
  - GlobDirRef
  - Make
    
    E
    
    U
  - Modules
  - NAMETREE
  - UserName
- Summary
  - Dyn
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
  - FrozenStage
  - Interp
  - Stage
  - Synterp
coq-core.parsing
- CLexer
  - Error
  - Lexer
    
    State
  - LexerDiff
    
    State
- Extend
- G_constr
- G_prim
- Notgram_ops
- Pcoq
  - Constr
  - Entry
  - GramState
  - Lookahead
  - Module
  - Parsable
  - Prim
  - Production
  - Rule
  - Rules
  - Symbol
- Tok
coq-core.perf
- Perf
coq-core.plugins.btauto
- Btauto_plugin
  - G_btauto
  - Refl_btauto
    
    Btauto
coq-core.plugins.cc
- Cc_plugin
  - Ccalgo
    
    ATerm
  - Ccproof
  - Cctac
  - G_congruence
coq-core.plugins.derive
- Derive_plugin
  - Derive
  - G_derive
coq-core.plugins.extraction
- Extraction_plugin
  - Common
  - Extract_env
  - Extraction
  - G_extraction
  - Haskell
  - Json
  - Miniml
  - Mlutil
    
    Mlenv
  - Modutil
  - Ocaml
  - Scheme
  - Table
    
    Refmap'
    
    Refset'
coq-core.plugins.firstorder
- Firstorder_plugin
  - Formula
  - G_ground
  - Ground
  - Instances
  - Rules
  - Sequent
  - Unify
    
    Item
coq-core.plugins.funind
- Funind_plugin
coq-core.plugins.ltac
- Ltac_plugin
  - ComRewrite
  - Coretactics
  - Extraargs
  - Extratactics
  - G_auto
  - G_class
  - G_eqdecide
  - G_ltac
  - G_obligations
  - G_rewrite
  - G_tactic
  - Internals
  - Leminv
  - Pltac
  - Pptactic
  - Profile_ltac
  - Profile_ltac_tactics
  - Tacarg
  - Taccoerce
    
    Value
  - Tacentries
  - Tacenv
  - Tacexpr
  - Tacintern
  - Tacinterp
    
    TacStore
    
    Value
  - Tacsubst
  - Tactic_debug
  - Tactic_matching
  - Tactic_option
coq-core.plugins.ltac2
- Ltac2_plugin
  - G_ltac2
  - Tac2bt
  - Tac2core
    
    Core
    
    MapType
    
    M
    
    Monad
    
    M
    
    Smart
    
    S
  - Tac2dyn
    
    Arg
    
    ArgMap
    
    M
    
    Param
    
    Val
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
  - Tac2entries
    
    Pltac
  - Tac2env
  - Tac2expr
    
    PartialPat
  - Tac2externals
  - Tac2extffi
  - Tac2ffi
    
    Valexpr
  - Tac2intern
  - Tac2interp
  - Tac2match
  - Tac2print
  - Tac2qexpr
  - Tac2quote
  - Tac2stdlib
  - Tac2tactics
  - Tac2types
  - Tac2typing_env
    
    TVar
    
    Map
coq-core.plugins.micromega
- Micromega_plugin
  - Certificate
  - Coq_micromega
  - G_micromega
  - Itv
  - Linsolve
  - Micromega
    
    Coq_Pos
    
    N
    
    Pos
    
    Z
  - Mutils
    
    CamlToCoq
    
    Cmp
    
    CoqToCaml
    
    Hash
    
    IMap
    
    Monad
    
    M
    
    Smart
    
    ISet
    
    McPrinter
    
    Tag
    
    TagSet
  - NumCompat
    
    Q
    
    Notations
    
    QArith
    
    Notations
    
    Z
    
    Z
    
    ZArith
  - Persistent_cache
    
    PHashtable
  - Polynomial
    
    BoundWithProof
    
    LinPoly
    
    MonT
    
    MonMap
    
    Monomial
    
    Poly
    
    ProofFormat
    
    Env
    
    WithProof
  - Simplex
  - Sos
  - Sos_lib
  - Sos_types
  - Vect
    
    Bound
coq-core.plugins.nsatz
- Nsatz_plugin
  - G_nsatz
  - Ideal
    
    Make
    
    P
    
    Monomial
  - Nsatz
  - Polynom
    
    Coef
    
    Make
    
    C
    
    S
  - Utile
coq-core.plugins.number_string_notation
- Number_string_notation_plugin
coq-core.plugins.ring
- Ring_plugin
  - G_ring
  - Ring
  - Ring_ast
coq-core.plugins.rtauto
- Rtauto_plugin
coq-core.plugins.ssreflect
- Ssreflect_plugin
  - Ssrast
  - Ssrbwd
  - Ssrcommon
    
    MakeState
    
    S
    
    StateType
  - Ssrelim
  - Ssrequality
  - Ssrfwd
  - Ssripats
    
    Internal
  - Ssrparser
    
    Internal
  - Ssrprinters
  - Ssrtacs
  - Ssrtacticals
  - Ssrvernac
  - Ssrview
    
    AdaptorDb
coq-core.plugins.ssrmatching
- Ssrmatching_plugin
  - G_ssrmatching
  - Ssrmatching
    
    Internal
coq-core.plugins.tauto
- Tauto_plugin
  - Tauto
coq-core.plugins.tutorial.p0
- Tuto0_plugin
  - G_tuto0
  - Tuto0_main
coq-core.plugins.tutorial.p1
- Tuto1_plugin
coq-core.plugins.tutorial.p2
- Tuto2_plugin
coq-core.plugins.tutorial.p3
- Tuto3_plugin
coq-core.plugins.zify
- Zify_plugin
  - G_zify
  - Zify
    
    BinOp
    
    BinOpSpec
    
    BinRel
    
    CstOp
    
    InjTable
    
    PropBinOp
    
    PropUnOp
    
    S
    
    Saturate
    
    UnOp
    
    UnOpSpec
coq-core.pretyping
- Arguments_renaming
- Cases
- Cbv
- Coercion
- Coercionops
- Constr_matching
- Detyping
  - PrintingInductiveMake
    
    Test
- Evarconv
- Evardefine
- Evarsolve
  - AllowedEvars
- Find_subterm
- Genarg
  - ArgT
  - GenObj
  - Register
    
    M
- Geninterp
  - TacStore
  - Val
  - ValTMap
    
    Value
- Gensubst
- GlobEnv
- Glob_ops
- Heads
- Indrec
- Inductiveops
- Keys
- Locusops
- Nativenorm
- Patternops
- Pretype_errors
- Pretyping
- Program
- Reductionops
- Retyping
- Structures
- Tacred
- Typeclasses
- Typeclasses_errors
- Typing
- Unification
- Vnorm
coq-core.printing
- Genprint
- Ppconstr
- Ppextend
- Pputils
- Printer
  - ContextObjectMap
    
    Monad
    
    M
    
    Smart
  - Debug
- Proof_diffs
coq-core.proofs
- Clenv
  - Internal
- Goal_select
- Logic
- Miscprint
- Proof
- Proof_bullet
- Refine
- Tacmach
coq-core.stm
- AsyncTaskQueue
  - MakeQueue
    
    T
  - MakeWorker
    
    T
  - Task
- Dag
  - Make
    
    Property
  - S
    
    Property
- Partac
  - TacTask
- ProofBlockDelimiter
- Spawned
- Stm
  - AsyncOpts
  - DynBlockData
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
  - ProofTask
  - QueryTask
- Stmargs
- TQueue
- Vcs
  - Kind
  - Make
    
    Branch
    
    Dag
    
    Property
    
    K
  - S
    
    Branch
    
    Dag
    
    Property
- Vio_checking
- WorkerPool
  - Make
    
    Model
  - PoolModel
coq-core.sysinit
coq-core.tactics
- Abstract
- Auto
- Autorewrite
  - RewRule
- Btermdn
  - Make
- Cbn
- Class_tactics
  - Search
- Contradiction
- DeclareScheme
- Dn
  - Make
- EClause
- Eauto
- Elim
- Elimschemes
- Eqdecide
- Eqschemes
- Equality
- Evar_tactics
- Generalize
- Hints
  - FullHint
  - Hint_db
- Hipattern
- Ind_tables
  - Locmap
- Induction
- Inv
- Ppred
- Redexpr
- Redops
- Rewrite
  - Internal
- Tacticals
- Tactics
  - Internal
  - Simple
coq-core.top_printers
- Top_printers
coq-core.toplevel
- Ccompile
- Colors
- Common_compile
- Coqc
- Coqcargs
- Coqloop
- Coqrc
- Coqtop
- G_toplevel
- Load
- Memtrace_init
- Vernac
  - State
- Vio_compile
- WorkerLoop
coq-core.vernac
- Assumptions
- Attributes
  - Notations
- Auto_ind_decl
- Canonical
- Classes
  - Event
  - Internal
- ComArguments
- ComAssumption
- ComCoercion
- ComDefinition
- ComExtraDeps
- ComFixpoint
- ComHints
- ComInductive
  - Internal
  - Mind_decl
- ComPrimitive
- ComProgramFixpoint
- ComSearch
- ComTactic
- DebugHook
  - Action
  - Answer
  - Intf
- Declare
  - CInfo
  - Hook
    
    S
  - Info
  - Internal
    
    Constant
  - OblState
    
    View
    
    Obl
  - Obls
  - Proof
- DeclareInd
  - Internal
- DeclareUniv
- Declaremods
  - Interp
  - Synterp
- Egramcoq
- Egramml
- Future
  - UUID
- G_proofs
- G_vernac
- Himsg
- Indschemes
- Library
- Loadpath
- Locality
- Metasyntax
- Mltop
  - PluginSpec
- Opaques
  - Summary
- Ppvernac
- Prettyp
- Printmod
- Proof_using
- Pvernac
  - Unsafe
  - Vernac_
- RecLemmas
- Record
  - Ast
  - Data
  - Internal
  - Record_decl
- RetrieveObl
- Search
- Synterp
- Topfmt
- Vernac_classifier
- Vernacentries
  - Preprocessed_Mind_decl
- Vernacextend
- Vernacinterp
- Vernacoptions
- Vernacprop
- Vernacstate
  - Declare
  - Interp
  - LemmaStack
  - Parser
  - Stm
  - Synterp
  - System
    
    Interp
    
    Synterp
- Vernactypes
  - InProg
  - InProof
  - OutProg
  - OutProof
coq-core.vm
- Coqrun

Legend:
Library
Module
Module type
Parameter
Class
Class type

This module registers the declaration of global tables, which will be kept in synchronization during the various backtracks of the system.

type t =

| Synterp
| Interp

We distinguish two stages and separate the system state accordingly. Synterp is the syntactic interpretation phase, i.e. vernacular parsing and execution of commands having an effect on parsing. Interp is the interpretation phase, where standard commands are executed.

val equal : t -> t -> bool