package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

package coq-core

coq-core
- Library btauto_plugin
  - Btauto_plugin
    
    G_btauto
    
    Refl_btauto
    
    Btauto
- Library cc_plugin
  - Cc_plugin
    
    Ccalgo
    
    ATerm
    
    Ccproof
    
    Cctac
    
    G_congruence
- Library coq-core.boot
  - Boot
    
    Env
    
    Path
    
    Path
    
    Usage
    
    Util
- Library coq-core.clib
  - CArray
    
    S
    
    ExtS
    
    Smart
    
    Fun1
    
    Smart
    
    Smart
    
    Fun1
    
    Smart
  - CEphemeron
  - CList
    
    Smart
    
    MonoS
  - CMap
    
    OrderedType
    
    MonadS
    
    S
    
    ExtS
    
    Set
    
    Smart
    
    Monad
    
    Make
    
    Smart
    
    Monad
  - CObj
  - CSet
    
    OrderedType
    
    S
    
    Make
    
    HashedType
    
    Hashcons
  - CSig
    
    SetS
    
    MapS
  - CString
    
    S
    
    ExtS
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    Pred
    
    List
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    Pred
    
    List
  - CThread
  - CUnix
  - Diff2
    
    SeqType
    
    S
    
    Make
  - Dyn
    
    ValueS
    
    MapS
    
    S
    
    Map
    
    HMap
    
    Easy
    
    Make
    
    Map
    
    HMap
    
    Easy
  - Exninfo
  - HMap
    
    HashedType
    
    Make
    
    Set
    
    Smart
    
    Monad
  - Hashcons
    
    HashconsedType
    
    S
    
    Make
    
    HashedType
    
    Hstring
    
    Hlist
  - Hashset
    
    EqType
    
    S
    
    Make
    
    Combine
  - Heap
    
    Ordered
    
    S
    
    Functional
  - IStream
  - Int
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    List
    
    PArray
    
    PMap
  - Monad
    
    Def
    
    ListS
    
    S
    
    List
    
    Make
    
    List
  - NeList
  - Option
    
    Smart
    
    List
  - OrderedType
    
    S
    
    Pair
    
    UnorderedPair
  - PolyMap
    
    ValueS
    
    Tag
    
    Make
    
    OneTag
    
    MapS
    
    Map
  - Predicate
    
    OrderedType
    
    S
    
    Make
  - Range
  - SList
    
    Skip
    
    Smart
  - Segmenttree
  - Store
    
    S
    
    Make
  - Terminal
  - Trie
    
    S
    
    Grp
    
    Make
  - Unicode
  - Unicodetable
  - Unionfind
    
    PartitionSig
    
    SetS
    
    MapS
    
    Make
- Library coq-core.config
  - Coq_config
- Library coq-core.coqworkmgrapi
  - CoqworkmgrApi
- Library coq-core.engine
  - EConstr
    
    ESorts
    
    EInstance
    
    UnsafeMonomorphic
    
    Vars
    
    Unsafe
  - Evar_kinds
  - Evarutil
    
    VarSet
  - Evd
    
    Filter
    
    Abstraction
    
    FutureGoals
    
    Store
    
    MonadR
    
    List
    
    Monad
    
    List
    
    Metaset
    
    Metamap
    
    Smart
    
    Monad
    
    MiniEConstr
    
    ESorts
    
    EInstance
  - Ftactic
    
    List
    
    Notations
  - Logic_monad
    
    NonLogical
    
    List
    
    BackState
    
    Param
    
    Logical
    
    List
    
    Unsafe
  - Namegen
  - Nameops
    
    Subscript
    
    Name
  - Proofview
    
    Monad
    
    List
    
    Progress
    
    Unsafe
    
    UnsafeRepr
    
    Goal
    
    Trace
    
    NonLogical
    
    List
    
    Notations
  - Proofview_monad
    
    Trace
    
    Info
    
    StateStore
    
    P
    
    Logical
    
    List
    
    Unsafe
    
    State
    
    Reader
    
    Writer
    
    Pv
    
    Solution
    
    Comb
    
    Env
    
    Status
    
    InfoL
  - Termops
    
    Internal
  - UState
    
    Internal
  - UnivGen
  - UnivMinim
    
    UPairSet
  - UnivNames
  - UnivProblem
    
    Set
  - UnivSubst
- Library coq-core.gramlib
  - Gramlib
    
    Gramext
    
    Grammar
    
    S
    
    Parsable
    
    Entry
    
    Symbol
    
    Rule
    
    Rules
    
    Production
    
    ExtS
    
    EState
    
    GState
    
    Parsable
    
    Entry
    
    Symbol
    
    Rule
    
    Rules
    
    Production
    
    Unsafe
    
    GMake
    
    EState
    
    GState
    
    Parsable
    
    Entry
    
    Symbol
    
    Rule
    
    Rules
    
    Production
    
    Unsafe
    
    LStream
    
    Plexing
    
    S
    
    State
    
    Stream
- Library coq-core.interp
  - Abbreviation
  - Constrexpr
  - Constrexpr_ops
  - Constrextern
  - Constrintern
  - Decls
  - Dumpglob
  - Genintern
    
    Store
  - Impargs
  - Implicit_quantifiers
  - Modintern
  - Notation
    
    NotationSet
    
    NotationMap
    
    Smart
    
    Monad
    
    SpecificNotationSet
    
    SpecificNotationMap
    
    Smart
    
    Monad
  - Notation_ops
  - Notation_term
  - Notationextern
  - NumTok
    
    UnsignedNat
    
    SignedNat
    
    Unsigned
    
    Signed
  - Reserve
  - Smartlocate
  - Stdarg
- Library coq-core.kernel
  - CClosure
    
    RedFlags
    
    KeyTable
  - CPrimitives
  - Constant_typing
  - Constr
    
    UnsafeMonomorphic
  - Context
    
    Rel
    
    Declaration
    
    Named
    
    Declaration
    
    Compacted
    
    Declaration
  - Conv_oracle
  - Conversion
  - Cooking
  - Declarations
  - Declareops
  - Discharge
  - Entries
  - Environ
    
    Globals
    
    QNameS
    
    QConstant
    
    QMutInd
    
    QInd
    
    QConstruct
    
    QProjection
    
    Repr
    
    QGlobRef
  - Esubst
    
    Internal
  - Evar
    
    Set
    
    Map
    
    Smart
    
    Monad
  - Float64
  - Float64_common
  - Genlambda
    
    S
    
    Make
  - IndTyping
  - Indtypes
  - Inductive
  - InferCumulativity
  - Mod_subst
  - Mod_typing
  - Modops
  - Names
    
    Id
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    Pred
    
    List
    
    Name
    
    ModIdset
    
    ModIdmap
    
    Smart
    
    Monad
    
    DirPath
    
    DPset
    
    DPmap
    
    Smart
    
    Monad
    
    Label
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    MBId
    
    MBIset
    
    MBImap
    
    Smart
    
    Monad
    
    ModPath
    
    MPset
    
    MPmap
    
    Smart
    
    Monad
    
    KerName
    
    KNset
    
    KNpred
    
    KNmap
    
    Smart
    
    Monad
    
    EqType
    
    QNameS
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    Constant
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    Cpred
    
    Cset
    
    Cset_env
    
    Cmap
    
    Smart
    
    Monad
    
    Cmap_env
    
    Smart
    
    Monad
    
    MutInd
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    Mindset
    
    Mindmap
    
    Smart
    
    Monad
    
    Mindmap_env
    
    Set
    
    Smart
    
    Monad
    
    Ind
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    Construct
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    Indset
    
    Constrset
    
    Indset_env
    
    Constrset_env
    
    Indmap
    
    Smart
    
    Monad
    
    Constrmap
    
    Smart
    
    Monad
    
    Indmap_env
    
    Smart
    
    Monad
    
    Constrmap_env
    
    Smart
    
    Monad
    
    Projection
    
    Repr
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    GlobRef
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    Set_env
    
    Map_env
    
    Smart
    
    Monad
    
    Set
    
    Map
    
    Smart
    
    Monad
  - Nativecode
  - Nativeconv
  - Nativelambda
  - Nativelib
  - Nativelibrary
  - Nativevalues
  - Opaqueproof
    
    HandleMap
  - Parray
  - Primred
    
    RedNativeEntries
    
    RedNative
    
    RedNative
  - Reduction
  - Relevanceops
  - Retroknowledge
  - Safe_typing
  - Section
  - Sorts
    
    QVar
  - Subtyping
  - Term
  - TransparentState
  - Type_errors
  - Typeops
  - UGraph
    
    Bound
  - Uint63
  - Univ
    
    UGlobal
    
    Level
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    Universe
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    Constraints
    
    Variance
    
    Instance
    
    UContext
    
    AbstractContext
    
    ContextSet
  - Values
  - Vars
  - Vconv
  - Vm
  - Vmbytecodes
    
    Label
  - Vmbytegen
  - Vmemitcodes
  - Vmlambda
  - Vmopcodes
  - Vmsymtable
  - Vmvalues
- Library coq-core.lib
  - AcyclicGraph
    
    Point
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    Make
  - Aux_file
    
    H
    
    M
  - CAst
    
    Smart
  - CDebug
  - CErrors
  - CProfile
  - CWarnings
    
    CoreCategories
  - Control
  - CoqProject_file
  - Core_plugins_findlib_compat
  - DAst
  - Deprecation
    
    Version
  - Envars
  - Feedback
  - Flags
  - Hook
  - Loc
  - ObjFile
  - Pp
  - Pp_diff
    
    StringDiff
  - Rtree
    
    Smart
  - Spawn
    
    Control
    
    MainLoopModel
    
    Async
    
    Sync
  - Stateid
    
    Self
    
    Set
  - System
  - Util
    
    Empty
    
    String
    
    List
    
    Smart
    
    MonoS
    
    Array
    
    Smart
    
    Fun1
    
    Smart
    
    Set
    
    OrderedType
    
    S
    
    Make
    
    HashedType
    
    Hashcons
    
    Map
    
    OrderedType
    
    MonadS
    
    S
    
    ExtS
    
    Set
    
    Smart
    
    Monad
    
    Make
    
    Smart
    
    Monad
    
    Union
  - Xml_datatype
- Library coq-core.library
  - Coqlib
  - Global
  - Globnames
    
    ExtRefOrdered
    
    ExtRefSet
    
    ExtRefMap
    
    Smart
    
    Monad
  - Goptions
    
    MakeStringTable
    
    MakeRefTable
    
    OptionMap
  - Lib
    
    StagedLibS
    
    Synterp
    
    Interp
  - Libnames
    
    Spmap
  - Libobject
    
    Dyn
    
    Map
    
    HMap
    
    Easy
  - Nametab
    
    GlobDirRef
    
    UnivIdMap
    
    Set
    
    Smart
    
    Monad
    
    UserName
    
    EqualityType
    
    NAMETREE
    
    Make
    
    Modules
  - Summary
    
    Stage
    
    Dyn
    
    Map
    
    HMap
    
    Easy
    
    Local
    
    FrozenStage
    
    Synterp
    
    Interp
- Library coq-core.parsing
  - CLexer
    
    Lexer
    
    State
    
    Error
    
    LexerDiff
    
    State
  - Extend
  - G_constr
  - G_prim
  - Notation_gram
  - Notgram_ops
  - Pcoq
    
    Parsable
    
    Entry
    
    Symbol
    
    Rule
    
    Rules
    
    Production
    
    Lookahead
    
    Prim
    
    Constr
    
    Module
    
    GramState
  - Tok
- Library coq-core.pretyping
  - Arguments_renaming
  - Cases
  - Cbv
  - Coercion
  - Coercionops
    
    ClTypSet
  - Constr_matching
  - Detyping
    
    PrintingInductiveMake
    
    Set
  - Evarconv
  - Evardefine
  - Evarsolve
    
    AllowedEvars
  - Find_subterm
  - Genarg
    
    ArgT
    
    GenObj
    
    Register
  - Geninterp
    
    Val
    
    ValTMap
    
    TacStore
  - GlobEnv
  - Glob_ops
  - Glob_term
  - Heads
  - Indrec
  - Inductiveops
  - Keys
  - Locus
  - Locusops
  - Ltac_pretype
  - Nativenorm
  - Pattern
  - Patternops
  - Pretype_errors
  - Pretyping
  - Program
  - Reductionops
    
    CredNative
    
    ReductionBehaviour
    
    Stack
  - Retyping
  - Structures
    
    Structure
    
    Instance
    
    ValuePattern
    
    CanonicalSolution
    
    CSTable
    
    PrimitiveProjections
  - Tacred
  - Typeclasses
  - Typeclasses_errors
  - Typing
  - Unification
  - Vnorm
- Library coq-core.printing
  - Genprint
  - Ppconstr
  - Ppextend
  - Pputils
  - Printer
    
    ContextObjectSet
    
    ContextObjectMap
    
    Smart
    
    Monad
    
    Debug
  - Proof_diffs
- Library coq-core.proofs
  - Clenv
    
    Internal
  - Goal_select
  - Logic
  - Miscprint
  - Proof
  - Proof_bullet
  - Refine
  - Tacmach
  - Tactypes
- Library coq-core.stm
  - AsyncTaskQueue
    
    Task
    
    MakeQueue
    
    MakeWorker
  - Dag
    
    S
    
    NodeSet
    
    Property
    
    Make
    
    NodeSet
    
    Property
  - Partac
    
    TacTask
  - ProofBlockDelimiter
  - Spawned
  - Stm
    
    AsyncOpts
    
    ProofTask
    
    QueryTask
    
    DynBlockData
    
    Map
    
    HMap
    
    Easy
  - Stmargs
  - TQueue
  - Vcs
    
    Kind
    
    S
    
    Branch
    
    Dag
    
    NodeSet
    
    Property
    
    Make
    
    Branch
    
    Dag
    
    NodeSet
    
    Property
  - Vio_checking
  - WorkerPool
    
    PoolModel
    
    Make
- Library coq-core.sysinit
- Library 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
  - Genredexpr
  - Hints
    
    FullHint
    
    Hint_db
  - Hipattern
  - Ind_tables
    
    Locmap
  - Inv
  - Ppred
  - Redexpr
  - Redops
  - Rewrite
    
    Internal
  - Tacticals
  - Tactics
    
    Simple
- Library coq-core.top_printers
  - Top_printers
- Library coq-core.toplevel
  - Ccompile
  - Colors
  - Common_compile
  - Coqc
  - Coqcargs
  - Coqloop
  - Coqrc
  - Coqtop
  - G_toplevel
  - Load
  - Memtrace_init
  - Vernac
    
    State
  - Vio_compile
  - WorkerLoop
- Library coq-core.vernac
  - Assumptions
  - Attributes
    
    Notations
  - Auto_ind_decl
  - Canonical
  - Classes
    
    Event
    
    Internal
  - ComArguments
  - ComAssumption
  - ComCoercion
  - ComDefinition
  - ComExtraDeps
  - ComFixpoint
  - ComHints
  - ComInductive
    
    Mind_decl
    
    Internal
  - ComPrimitive
  - ComProgramFixpoint
  - ComSearch
  - ComTactic
  - DebugHook
    
    Action
    
    Answer
    
    Intf
  - Declare
    
    Hook
    
    S
    
    CInfo
    
    Info
    
    OblState
    
    View
    
    Obl
    
    Proof
    
    Obls
    
    Internal
    
    Constant
  - DeclareInd
    
    Internal
  - DeclareUctx
  - DeclareUniv
  - Declaremods
    
    Synterp
    
    Interp
  - Egramcoq
  - Egramml
  - Future
    
    UUID
    
    UUIDMap
    
    UUIDSet
  - G_proofs
  - G_vernac
  - Himsg
  - Indschemes
  - Library
  - Loadpath
  - Locality
  - Metasyntax
  - Mltop
    
    PluginSpec
  - Opaques
    
    Summary
  - Ppvernac
  - Prettyp
  - Printmod
  - Proof_using
  - Pvernac
    
    Vernac_
    
    Unsafe
  - RecLemmas
  - Record
    
    Ast
    
    Data
    
    Record_decl
    
    Internal
  - RetrieveObl
  - Search
  - Synterp
  - Topfmt
  - Vernac_classifier
  - Vernacentries
    
    Preprocessed_Mind_decl
  - Vernacexpr
  - Vernacextend
    
    InProg
    
    OutProg
    
    InProof
    
    OutProof
  - Vernacinterp
  - Vernacoptions
  - Vernacprop
  - Vernacstate
    
    Parser
    
    System
    
    Synterp
    
    Interp
    
    Synterp
    
    LemmaStack
    
    Interp
    
    Stm
    
    Declare
- Library coq-core.vm
  - Coqrun
- Library derive_plugin
  - Derive_plugin
    
    Derive
    
    G_derive
- Library extraction_plugin
  - Extraction_plugin
    
    Common
    
    Extract_env
    
    Extraction
    
    G_extraction
    
    Haskell
    
    Json
    
    Miniml
    
    Mlutil
    
    Mlenv
    
    Modutil
    
    Ocaml
    
    Scheme
    
    Table
    
    Refset'
    
    Refmap'
- Library firstorder_plugin
  - Firstorder_plugin
    
    Formula
    
    G_ground
    
    Ground
    
    Instances
    
    Rules
    
    Sequent
    
    Unify
    
    Item
- Library funind_plugin
  - Funind_plugin
    
    Functional_principles_proofs
    
    Functional_principles_types
    
    G_indfun
    
    Gen_principle
    
    Glob_term_to_relation
    
    Glob_termops
    
    Indfun
    
    Indfun_common
    
    Invfun
    
    Recdef
- Library ltac2_plugin
  - Ltac2_plugin
    
    G_ltac2
    
    Tac2bt
    
    Tac2core
    
    Core
    
    MapType
    
    S
    
    M
    
    Smart
    
    Monad
    
    Tac2dyn
    
    Arg
    
    Param
    
    ArgMap
    
    Val
    
    Map
    
    HMap
    
    Easy
    
    Tac2entries
    
    Pltac
    
    Tac2env
    
    Tac2expr
    
    PartialPat
    
    Tac2extffi
    
    Tac2ffi
    
    Valexpr
    
    Tac2intern
    
    Tac2interp
    
    Tac2match
    
    Tac2print
    
    Tac2qexpr
    
    Tac2quote
    
    Tac2stdlib
    
    Tac2tactics
    
    Tac2types
    
    Tac2typing_env
    
    TVar
    
    Map
- Library ltac_plugin
  - 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
    
    Value
    
    TacStore
    
    Tacsubst
    
    Tactic_debug
    
    Tactic_matching
    
    Tactic_option
- Library micromega_plugin
  - Micromega_plugin
    
    Certificate
    
    Mc
    
    Coq_micromega
    
    G_micromega
    
    Itv
    
    Linsolve
    
    Micromega
    
    Pos
    
    Coq_Pos
    
    N
    
    Z
    
    Mutils
    
    Int
    
    ISet
    
    IMap
    
    Cmp
    
    Tag
    
    TagSet
    
    McPrinter
    
    Mc
    
    CamlToCoq
    
    CoqToCaml
    
    Hash
    
    NumCompat
    
    ZArith
    
    QArith
    
    Z
    
    Notations
    
    Z
    
    Q
    
    Z
    
    Notations
    
    Persistent_cache
    
    PHashtable
    
    PHashtable
    
    Polynomial
    
    Mc
    
    Monomial
    
    MonMap
    
    Poly
    
    LinPoly
    
    MonT
    
    ProofFormat
    
    Env
    
    PrfRuleMap
    
    WithProof
    
    BoundWithProof
    
    Simplex
    
    Sos
    
    Sos_lib
    
    Sos_types
    
    Vect
    
    Bound
- Library nsatz_plugin
  - Nsatz_plugin
    
    G_nsatz
    
    Ideal
    
    Monomial
    
    Make
    
    Hashpol
    
    Nsatz
    
    Polynom
    
    Coef
    
    S
    
    Hashpol
    
    Make
    
    Hashpol
    
    Utile
- Library number_string_notation_plugin
  - Number_string_notation_plugin
    
    G_number_string
    
    Number
    
    String_notation
- Library ring_plugin
  - Ring_plugin
    
    G_ring
    
    Ring
    
    Ring_ast
- Library rtauto_plugin
  - Rtauto_plugin
    
    G_rtauto
    
    Proof_search
    
    Refl_tauto
- Library ssreflect_plugin
  - Ssreflect_plugin
    
    Ssrast
    
    Ssrbwd
    
    Ssrcommon
    
    StateType
    
    MakeState
    
    Ssrelim
    
    Ssrequality
    
    Ssrfwd
    
    Ssripats
    
    Internal
    
    Ssrparser
    
    Internal
    
    Ssrprinters
    
    Ssrtacs
    
    Ssrtacticals
    
    Ssrvernac
    
    Ssrview
    
    AdaptorDb
- Library ssrmatching_plugin
  - Ssrmatching_plugin
    
    G_ssrmatching
    
    Ssrmatching
    
    Internal
- Library tauto_plugin
  - Tauto_plugin
    
    Tauto
- Library tuto0_plugin
  - Tuto0_plugin
    
    G_tuto0
    
    Tuto0_main
- Library tuto1_plugin
  - Tuto1_plugin
    
    G_tuto1
    
    Inspector
    
    Simple_check
    
    Simple_declare
    
    Simple_print
- Library tuto2_plugin
  - Tuto2_plugin
    
    Counter
    
    Custom
    
    G_tuto2
    
    Persistent_counter
- Library tuto3_plugin
  - Tuto3_plugin
    
    Construction_game
    
    G_tuto3
    
    Tuto_tactic
- Library zify_plugin
  - Zify_plugin
    
    G_zify
    
    Zify
    
    S
    
    InjTable
    
    UnOp
    
    BinOp
    
    CstOp
    
    BinRel
    
    PropBinOp
    
    PropUnOp
    
    BinOpSpec
    
    UnOpSpec
    
    Saturate
- Sources
  - btauto_plugin
    
    btauto_plugin.ml
    
    g_btauto.ml
    
    refl_btauto.ml
  - cc_plugin
    
    cc_plugin.ml
    
    ccalgo.ml
    
    ccproof.ml
    
    cctac.ml
    
    g_congruence.ml
  - coq-core.boot
    
    boot.ml
    
    env.ml
    
    path.ml
    
    usage.ml
    
    util.ml
  - coq-core.clib
    
    cArray.ml
    
    cEphemeron.ml
    
    cList.ml
    
    cMap.ml
    
    cObj.ml
    
    cSet.ml
    
    cString.ml
    
    cThread.ml
    
    cUnix.ml
    
    diff2.ml
    
    dyn.ml
    
    exninfo.ml
    
    hMap.ml
    
    hashcons.ml
    
    hashset.ml
    
    heap.ml
    
    iStream.ml
    
    int.ml
    
    monad.ml
    
    neList.ml
    
    option.ml
    
    orderedType.ml
    
    polyMap.ml
    
    predicate.ml
    
    range.ml
    
    sList.ml
    
    segmenttree.ml
    
    store.ml
    
    terminal.ml
    
    trie.ml
    
    unicode.ml
    
    unicodetable.ml
    
    unionfind.ml
  - coq-core.config
    
    coq_config.ml
  - coq-core.coqworkmgrapi
    
    coqworkmgrApi.ml
  - coq-core.engine
    
    eConstr.ml
    
    evar_kinds.ml
    
    evarutil.ml
    
    evd.ml
    
    ftactic.ml
    
    logic_monad.ml
    
    namegen.ml
    
    nameops.ml
    
    proofview.ml
    
    proofview_monad.ml
    
    termops.ml
    
    uState.ml
    
    univGen.ml
    
    univMinim.ml
    
    univNames.ml
    
    univProblem.ml
    
    univSubst.ml
  - coq-core.gramlib
    
    gramext.ml
    
    gramlib.ml
    
    grammar.ml
    
    lStream.ml
    
    stream.ml
  - coq-core.interp
    
    abbreviation.ml
    
    constrexpr_ops.ml
    
    constrextern.ml
    
    constrintern.ml
    
    decls.ml
    
    dumpglob.ml
    
    genintern.ml
    
    impargs.ml
    
    implicit_quantifiers.ml
    
    modintern.ml
    
    notation.ml
    
    notation_ops.ml
    
    notationextern.ml
    
    numTok.ml
    
    reserve.ml
    
    smartlocate.ml
    
    stdarg.ml
  - coq-core.kernel
    
    cClosure.ml
    
    cPrimitives.ml
    
    constant_typing.ml
    
    constr.ml
    
    context.ml
    
    conv_oracle.ml
    
    conversion.ml
    
    cooking.ml
    
    declareops.ml
    
    discharge.ml
    
    environ.ml
    
    esubst.ml
    
    evar.ml
    
    float64.ml
    
    float64_common.ml
    
    genlambda.ml
    
    indTyping.ml
    
    indtypes.ml
    
    inductive.ml
    
    inferCumulativity.ml
    
    mod_subst.ml
    
    mod_typing.ml
    
    modops.ml
    
    names.ml
    
    nativecode.ml
    
    nativeconv.ml
    
    nativelambda.ml
    
    nativelib.ml
    
    nativelibrary.ml
    
    nativevalues.ml
    
    opaqueproof.ml
    
    parray.ml
    
    primred.ml
    
    reduction.ml
    
    relevanceops.ml
    
    retroknowledge.ml
    
    safe_typing.ml
    
    section.ml
    
    sorts.ml
    
    subtyping.ml
    
    term.ml
    
    transparentState.ml
    
    type_errors.ml
    
    typeops.ml
    
    uGraph.ml
    
    uint63.ml
    
    univ.ml
    
    vars.ml
    
    vconv.ml
    
    vm.ml
    
    vmbytecodes.ml
    
    vmbytegen.ml
    
    vmemitcodes.ml
    
    vmlambda.ml
    
    vmopcodes.ml
    
    vmsymtable.ml
    
    vmvalues.ml
  - coq-core.lib
    
    acyclicGraph.ml
    
    aux_file.ml
    
    cAst.ml
    
    cDebug.ml
    
    cErrors.ml
    
    cProfile.ml
    
    cWarnings.ml
    
    control.ml
    
    coqProject_file.ml
    
    core_plugins_findlib_compat.ml
    
    dAst.ml
    
    deprecation.ml
    
    envars.ml
    
    feedback.ml
    
    flags.ml
    
    hook.ml
    
    loc.ml
    
    objFile.ml
    
    pp.ml
    
    pp_diff.ml
    
    rtree.ml
    
    spawn.ml
    
    stateid.ml
    
    system.ml
    
    util.ml
  - coq-core.library
    
    coqlib.ml
    
    global.ml
    
    globnames.ml
    
    goptions.ml
    
    lib.ml
    
    libnames.ml
    
    libobject.ml
    
    nametab.ml
    
    summary.ml
  - coq-core.parsing
    
    cLexer.ml
    
    extend.ml
    
    g_constr.ml
    
    g_prim.ml
    
    notgram_ops.ml
    
    pcoq.ml
    
    tok.ml
  - coq-core.pretyping
    
    arguments_renaming.ml
    
    cases.ml
    
    cbv.ml
    
    coercion.ml
    
    coercionops.ml
    
    constr_matching.ml
    
    detyping.ml
    
    evarconv.ml
    
    evardefine.ml
    
    evarsolve.ml
    
    find_subterm.ml
    
    genarg.ml
    
    geninterp.ml
    
    globEnv.ml
    
    glob_ops.ml
    
    heads.ml
    
    indrec.ml
    
    inductiveops.ml
    
    keys.ml
    
    locusops.ml
    
    nativenorm.ml
    
    patternops.ml
    
    pretype_errors.ml
    
    pretyping.ml
    
    program.ml
    
    reductionops.ml
    
    retyping.ml
    
    structures.ml
    
    tacred.ml
    
    typeclasses.ml
    
    typeclasses_errors.ml
    
    typing.ml
    
    unification.ml
    
    vnorm.ml
  - coq-core.printing
    
    genprint.ml
    
    ppconstr.ml
    
    ppextend.ml
    
    pputils.ml
    
    printer.ml
    
    proof_diffs.ml
  - coq-core.proofs
    
    clenv.ml
    
    goal_select.ml
    
    logic.ml
    
    miscprint.ml
    
    proof.ml
    
    proof_bullet.ml
    
    refine.ml
    
    tacmach.ml
  - coq-core.stm
    
    asyncTaskQueue.ml
    
    dag.ml
    
    partac.ml
    
    proofBlockDelimiter.ml
    
    spawned.ml
    
    stm.ml
    
    stmargs.ml
    
    tQueue.ml
    
    vcs.ml
    
    vio_checking.ml
    
    workerPool.ml
  - coq-core.sysinit
    
    coqargs.ml
    
    coqinit.ml
    
    coqloadpath.ml
  - coq-core.tactics
    
    abstract.ml
    
    auto.ml
    
    autorewrite.ml
    
    btermdn.ml
    
    cbn.ml
    
    class_tactics.ml
    
    contradiction.ml
    
    declareScheme.ml
    
    dn.ml
    
    eClause.ml
    
    eauto.ml
    
    elim.ml
    
    elimschemes.ml
    
    eqdecide.ml
    
    eqschemes.ml
    
    equality.ml
    
    evar_tactics.ml
    
    hints.ml
    
    hipattern.ml
    
    ind_tables.ml
    
    inv.ml
    
    ppred.ml
    
    redexpr.ml
    
    redops.ml
    
    rewrite.ml
    
    tacticals.ml
    
    tactics.ml
  - coq-core.top_printers
    
    top_printers.ml
  - coq-core.toplevel
    
    ccompile.ml
    
    colors.ml
    
    common_compile.ml
    
    coqc.ml
    
    coqcargs.ml
    
    coqloop.ml
    
    coqrc.ml
    
    coqtop.ml
    
    g_toplevel.ml
    
    load.ml
    
    memtrace_init.ml
    
    vernac.ml
    
    vio_compile.ml
    
    workerLoop.ml
  - coq-core.vernac
    
    assumptions.ml
    
    attributes.ml
    
    auto_ind_decl.ml
    
    canonical.ml
    
    classes.ml
    
    comArguments.ml
    
    comAssumption.ml
    
    comCoercion.ml
    
    comDefinition.ml
    
    comExtraDeps.ml
    
    comFixpoint.ml
    
    comHints.ml
    
    comInductive.ml
    
    comPrimitive.ml
    
    comProgramFixpoint.ml
    
    comSearch.ml
    
    comTactic.ml
    
    debugHook.ml
    
    declare.ml
    
    declareInd.ml
    
    declareUctx.ml
    
    declareUniv.ml
    
    declaremods.ml
    
    egramcoq.ml
    
    egramml.ml
    
    future.ml
    
    g_proofs.ml
    
    g_vernac.ml
    
    himsg.ml
    
    indschemes.ml
    
    library.ml
    
    loadpath.ml
    
    locality.ml
    
    metasyntax.ml
    
    mltop.ml
    
    opaques.ml
    
    ppvernac.ml
    
    prettyp.ml
    
    printmod.ml
    
    proof_using.ml
    
    pvernac.ml
    
    recLemmas.ml
    
    record.ml
    
    retrieveObl.ml
    
    search.ml
    
    synterp.ml
    
    topfmt.ml
    
    vernac_classifier.ml
    
    vernacentries.ml
    
    vernacextend.ml
    
    vernacinterp.ml
    
    vernacoptions.ml
    
    vernacprop.ml
    
    vernacstate.ml
  - coq-core.vm
    
    coqrun.ml
  - derive_plugin
    
    derive.ml
    
    derive_plugin.ml
    
    g_derive.ml
  - extraction_plugin
    
    common.ml
    
    extract_env.ml
    
    extraction.ml
    
    extraction_plugin.ml
    
    g_extraction.ml
    
    haskell.ml
    
    json.ml
    
    miniml.ml
    
    mlutil.ml
    
    modutil.ml
    
    ocaml.ml
    
    scheme.ml
    
    table.ml
  - firstorder_plugin
    
    firstorder_plugin.ml
    
    formula.ml
    
    g_ground.ml
    
    ground.ml
    
    instances.ml
    
    rules.ml
    
    sequent.ml
    
    unify.ml
  - funind_plugin
    
    functional_principles_proofs.ml
    
    functional_principles_types.ml
    
    funind_plugin.ml
    
    g_indfun.ml
    
    gen_principle.ml
    
    glob_term_to_relation.ml
    
    glob_termops.ml
    
    indfun.ml
    
    indfun_common.ml
    
    invfun.ml
    
    recdef.ml
  - ltac2_plugin
    
    g_ltac2.ml
    
    ltac2_plugin.ml
    
    tac2bt.ml
    
    tac2core.ml
    
    tac2dyn.ml
    
    tac2entries.ml
    
    tac2env.ml
    
    tac2extffi.ml
    
    tac2ffi.ml
    
    tac2intern.ml
    
    tac2interp.ml
    
    tac2match.ml
    
    tac2print.ml
    
    tac2quote.ml
    
    tac2stdlib.ml
    
    tac2tactics.ml
    
    tac2typing_env.ml
  - ltac_plugin
    
    comRewrite.ml
    
    coretactics.ml
    
    extraargs.ml
    
    extratactics.ml
    
    g_auto.ml
    
    g_class.ml
    
    g_eqdecide.ml
    
    g_ltac.ml
    
    g_obligations.ml
    
    g_rewrite.ml
    
    g_tactic.ml
    
    internals.ml
    
    leminv.ml
    
    ltac_plugin.ml
    
    pltac.ml
    
    pptactic.ml
    
    profile_ltac.ml
    
    profile_ltac_tactics.ml
    
    tacarg.ml
    
    taccoerce.ml
    
    tacentries.ml
    
    tacenv.ml
    
    tacexpr.ml
    
    tacintern.ml
    
    tacinterp.ml
    
    tacsubst.ml
    
    tactic_debug.ml
    
    tactic_matching.ml
    
    tactic_option.ml
  - micromega_plugin
    
    certificate.ml
    
    coq_micromega.ml
    
    g_micromega.ml
    
    itv.ml
    
    linsolve.ml
    
    micromega.ml
    
    micromega_plugin.ml
    
    mutils.ml
    
    numCompat.ml
    
    persistent_cache.ml
    
    polynomial.ml
    
    simplex.ml
    
    sos.ml
    
    sos_lib.ml
    
    sos_types.ml
    
    vect.ml
  - nsatz_plugin
    
    g_nsatz.ml
    
    ideal.ml
    
    nsatz.ml
    
    nsatz_plugin.ml
    
    polynom.ml
    
    utile.ml
  - number_string_notation_plugin
    
    g_number_string.ml
    
    number.ml
    
    number_string_notation_plugin.ml
    
    string_notation.ml
  - ring_plugin
    
    g_ring.ml
    
    ring.ml
    
    ring_ast.ml
    
    ring_plugin.ml
  - rtauto_plugin
    
    g_rtauto.ml
    
    proof_search.ml
    
    refl_tauto.ml
    
    rtauto_plugin.ml
  - ssreflect_plugin
    
    ssrbwd.ml
    
    ssrcommon.ml
    
    ssreflect_plugin.ml
    
    ssrelim.ml
    
    ssrequality.ml
    
    ssrfwd.ml
    
    ssripats.ml
    
    ssrparser.ml
    
    ssrprinters.ml
    
    ssrtacs.ml
    
    ssrtacticals.ml
    
    ssrvernac.ml
    
    ssrview.ml
  - ssrmatching_plugin
    
    g_ssrmatching.ml
    
    ssrmatching.ml
    
    ssrmatching_plugin.ml
  - tauto_plugin
    
    tauto.ml
    
    tauto_plugin.ml
  - tuto0_plugin
    
    g_tuto0.ml
    
    tuto0_main.ml
    
    tuto0_plugin.ml
  - tuto1_plugin
    
    g_tuto1.ml
    
    inspector.ml
    
    simple_check.ml
    
    simple_declare.ml
    
    simple_print.ml
    
    tuto1_plugin.ml
  - tuto2_plugin
    
    counter.ml
    
    custom.ml
    
    g_tuto2.ml
    
    persistent_counter.ml
    
    tuto2_plugin.ml
  - tuto3_plugin
    
    construction_game.ml
    
    g_tuto3.ml
    
    tuto3_plugin.ml
    
    tuto_tactic.ml
  - zify_plugin
    
    g_zify.ml
    
    zify.ml
    
    zify_plugin.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Reduction`Source

None of these functions do eta reduction

Sourceval whd_all : Environ.env -> Constr.constr -> Constr.constr

Sourceval beta_applist : Constr.constr -> Constr.constr list -> Constr.constr

Builds an application node, reducing beta redexes it may produce.

Sourceval beta_appvect : Constr.constr -> Constr.constr array -> Constr.constr

Builds an application node, reducing beta redexes it may produce.

Sourceval beta_app : Constr.constr -> Constr.constr -> Constr.constr

Builds an application node, reducing beta redexe it may produce.

Source

val hnf_prod_applist : 
  Environ.env ->
  Constr.types ->
  Constr.constr list ->
  Constr.types

Pseudo-reduction rule Prod(x,A,B) a --> Bx\a

Source

val hnf_prod_applist_decls : 
  Environ.env ->
  int ->
  Constr.types ->
  Constr.constr list ->
  Constr.types

In hnf_prod_applist_decls n c args, c is supposed to (whd-)reduce to the form ∀Γ.t with Γ of length n and possibly with let-ins; it returns t with the assumptions of Γ instantiated by args and the local definitions of Γ expanded.

Source

val betazeta_appvect : 
  int ->
  Constr.constr ->
  Constr.constr array ->
  Constr.constr

Compatibility alias for Term.lambda_appvect_decls

Source

val hnf_decompose_prod : 
  Environ.env ->
  Constr.types ->
  Constr.rel_context * Constr.types

Source

val hnf_decompose_prod_decls : 
  Environ.env ->
  Constr.types ->
  Constr.rel_context * Constr.types

Source

val hnf_decompose_lambda : 
  Environ.env ->
  Constr.constr ->
  Constr.rel_context * Constr.constr

Source

val hnf_decompose_lambda_decls : 
  Environ.env ->
  Constr.constr ->
  Constr.rel_context * Constr.constr

Source

val hnf_decompose_lambda_n_decls : 
  Environ.env ->
  int ->
  Constr.constr ->
  Constr.rel_context * Constr.constr

Sourceexception NotArity

Sourceval dest_arity : Environ.env -> Constr.types -> Term.arity

Sourceval is_arity : Environ.env -> Constr.types -> bool

Sourceval eta_expand : Environ.env -> Constr.constr -> Constr.types -> Constr.constr

Deprecated

Source

val dest_prod : 
  Environ.env ->
  Constr.types ->
  Constr.rel_context * Constr.types

deprecated Use [hnf_decompose_prod] instead.

Source

val dest_prod_assum : 
  Environ.env ->
  Constr.types ->
  Constr.rel_context * Constr.types

deprecated Use [hnf_decompose_prod_decls] instead.

Source

val dest_lam : 
  Environ.env ->
  Constr.constr ->
  Constr.rel_context * Constr.constr

deprecated Use [hnf_decompose_lambda] instead.

Source

val dest_lam_assum : 
  Environ.env ->
  Constr.constr ->
  Constr.rel_context * Constr.constr

deprecated Use [hnf_decompose_lambda_decls] instead.

package coq-core

Module ReductionSource

Module `Reduction`Source