package coq

You can search for identifiers within the package.

in-package search v0.2.0

package coq

coq
- Library btauto_plugin
  - Btauto_plugin
    
    G_btauto
    
    Refl_btauto
    
    Btauto
- Library cc_plugin
  - Cc_plugin
    
    Ccalgo
    
    PafMap
    
    PacMap
    
    ATerm
    
    Constrhash
    
    Termhash
    
    Ccproof
    
    Cctac
    
    G_congruence
- Library coq-core.boot
  - Boot
    
    Env
    
    Path
    
    Path
    
    Util
- Library coq-core.clib
  - CArray
    
    S
    
    ExtS
    
    Smart
    
    Fun1
    
    Smart
    
    Smart
    
    Fun1
    
    Smart
  - CEphemeron
  - CList
    
    S
    
    ExtS
    
    Smart
    
    MonoS
    
    Smart
    
    MonoS
  - CMap
    
    OrderedType
    
    MonadS
    
    S
    
    ExtS
    
    Set
    
    Smart
    
    Unsafe
    
    Monad
    
    Make
    
    Smart
    
    Unsafe
    
    Monad
  - CObj
  - CSet
    
    OrderedType
    
    S
    
    Make
    
    HashedType
    
    Hashcons
  - CSig
    
    SetS
    
    MapS
  - CString
    
    S
    
    ExtS
    
    Set
    
    Map
    
    Smart
    
    Unsafe
    
    Monad
    
    Pred
    
    List
    
    Set
    
    Map
    
    Smart
    
    Unsafe
    
    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
    
    Unsafe
    
    Monad
  - Hashcons
    
    HashconsedType
    
    S
    
    Make
    
    HashedType
    
    Hstring
    
    Hlist
  - Hashset
    
    EqType
    
    S
    
    Make
    
    Combine
  - Heap
    
    Ordered
    
    S
    
    Functional
  - IStream
  - Int
    
    Set
    
    Map
    
    Smart
    
    Unsafe
    
    Monad
    
    List
    
    PArray
    
    PMap
  - Minisys
  - Monad
    
    Def
    
    ListS
    
    S
    
    List
    
    Make
    
    List
  - NeList
  - Option
    
    Smart
    
    List
  - OrderedType
    
    S
    
    Pair
    
    UnorderedPair
  - Predicate
    
    OrderedType
    
    S
    
    Make
  - Range
  - 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.engine
  - EConstr
    
    ESorts
    
    EInstance
    
    Vars
    
    Unsafe
  - Evar_kinds
  - Evarutil
  - Evd
    
    Filter
    
    Abstraction
    
    Identity
    
    FutureGoals
    
    Store
    
    MonadR
    
    List
    
    Monad
    
    List
    
    Metaset
    
    Metamap
    
    Smart
    
    Unsafe
    
    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
  - Proofview_monad
    
    Trace
    
    Info
    
    StateStore
    
    P
    
    Logical
    
    List
    
    Unsafe
    
    State
    
    Reader
    
    Writer
    
    Pv
    
    Solution
    
    Comb
    
    Env
    
    Status
    
    InfoL
  - Termops
    
    Internal
  - UState
  - UnivGen
  - UnivMinim
    
    UPairSet
  - UnivNames
  - UnivProblem
    
    Set
  - UnivSubst
- Library coq-core.gramlib
  - Gramlib
    
    Gramext
    
    Grammar
    
    S
    
    Parsable
    
    Entry
    
    Symbol
    
    Rule
    
    Rules
    
    Production
    
    ExtS
    
    Parsable
    
    Entry
    
    Symbol
    
    Rule
    
    Rules
    
    Production
    
    Unsafe
    
    GMake
    
    Parsable
    
    Entry
    
    Symbol
    
    Rule
    
    Rules
    
    Production
    
    Unsafe
    
    Plexing
    
    S
    
    State
- Library coq-core.interp
  - Constrexpr
  - Constrexpr_ops
  - Constrextern
  - Constrintern
  - Decls
  - Deprecation
  - Dumpglob
  - Genintern
    
    Store
  - Impargs
  - Implicit_quantifiers
  - Modintern
  - Notation
    
    NotationSet
    
    NotationMap
    
    Smart
    
    Unsafe
    
    Monad
    
    SpecificNotationSet
    
    SpecificNotationMap
    
    Smart
    
    Unsafe
    
    Monad
  - Notation_ops
  - Notation_term
  - NumTok
    
    UnsignedNat
    
    SignedNat
    
    Unsigned
    
    Signed
  - Reserve
  - Smartlocate
  - Stdarg
  - Syntax_def
- Library coq-core.kernel
  - CClosure
    
    RedFlags
    
    KeyTable
  - CPrimitives
  - Constr
  - Context
    
    Rel
    
    Declaration
    
    Named
    
    Declaration
    
    Compacted
    
    Declaration
  - Conv_oracle
  - Cooking
  - Declarations
  - Declareops
  - Entries
  - Environ
    
    Globals
    
    QNameS
    
    QConstant
    
    QMutInd
    
    QInd
    
    QConstruct
    
    QProjection
    
    Repr
    
    QGlobRef
  - Esubst
    
    Internal
  - Evar
    
    Set
    
    Map
    
    Smart
    
    Unsafe
    
    Monad
  - Float64
  - Float64_common
  - IndTyping
  - Indtypes
  - Inductive
  - InferCumulativity
  - Mod_subst
  - Mod_typing
  - Modops
  - Names
    
    Id
    
    Set
    
    Map
    
    Smart
    
    Unsafe
    
    Monad
    
    Pred
    
    List
    
    Name
    
    ModIdset
    
    ModIdmap
    
    Smart
    
    Unsafe
    
    Monad
    
    DirPath
    
    DPset
    
    DPmap
    
    Smart
    
    Unsafe
    
    Monad
    
    Label
    
    Set
    
    Map
    
    Smart
    
    Unsafe
    
    Monad
    
    MBId
    
    MBIset
    
    MBImap
    
    Smart
    
    Unsafe
    
    Monad
    
    ModPath
    
    MPset
    
    MPmap
    
    Smart
    
    Unsafe
    
    Monad
    
    KerName
    
    KNset
    
    KNpred
    
    KNmap
    
    Smart
    
    Unsafe
    
    Monad
    
    EqType
    
    QNameS
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    Constant
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    Cpred
    
    Cset
    
    Cset_env
    
    Cmap
    
    Smart
    
    Unsafe
    
    Monad
    
    Cmap_env
    
    Smart
    
    Unsafe
    
    Monad
    
    MutInd
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    Mindset
    
    Mindmap
    
    Smart
    
    Unsafe
    
    Monad
    
    Mindmap_env
    
    Set
    
    Smart
    
    Unsafe
    
    Monad
    
    Ind
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    Construct
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    Indset
    
    Constrset
    
    Indset_env
    
    Constrset_env
    
    Indmap
    
    Smart
    
    Unsafe
    
    Monad
    
    Constrmap
    
    Smart
    
    Unsafe
    
    Monad
    
    Indmap_env
    
    Smart
    
    Unsafe
    
    Monad
    
    Constrmap_env
    
    Smart
    
    Unsafe
    
    Monad
    
    Projection
    
    Repr
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    GlobRef
    
    CanOrd
    
    UserOrd
    
    SyntacticOrd
    
    Set_env
    
    Map_env
    
    Smart
    
    Unsafe
    
    Monad
    
    Set
    
    Map
    
    Smart
    
    Unsafe
    
    Monad
  - Nativecode
  - Nativeconv
  - Nativelambda
  - Nativelib
  - Nativelibrary
  - Nativevalues
  - Opaqueproof
    
    HandleMap
  - Parray
  - Primred
    
    RedNativeEntries
    
    RedNative
    
    RedNative
  - Reduction
  - Relevanceops
  - Retroknowledge
  - Safe_typing
  - Section
  - Sorts
  - Subtyping
  - Term
  - Term_typing
  - TransparentState
  - Type_errors
  - Typeops
  - UGraph
    
    Bound
  - Uint63
  - Univ
    
    Level
    
    UGlobal
    
    Set
    
    Map
    
    Smart
    
    Unsafe
    
    Monad
    
    LSet
    
    Universe
    
    Set
    
    Map
    
    Smart
    
    Unsafe
    
    Monad
    
    Constraints
    
    Constraint
    
    LMap
    
    Smart
    
    Unsafe
    
    Monad
    
    Variance
    
    Instance
    
    UContext
    
    AbstractContext
    
    AUContext
    
    ContextSet
  - Vars
  - Vconv
  - Vm
  - Vmbytecodes
    
    Label
  - Vmbytegen
  - Vmemitcodes
  - Vmlambda
  - Vmopcodes
  - Vmsymtable
  - Vmvalues
- Library coq-core.lib
  - AcyclicGraph
    
    Point
    
    Set
    
    Map
    
    Smart
    
    Unsafe
    
    Monad
    
    Constraints
    
    Make
  - Aux_file
    
    H
    
    M
  - CAst
  - CDebug
  - CErrors
  - CProfile
  - CWarnings
  - Control
  - CoqProject_file
  - DAst
  - Envars
  - Explore
    
    SearchProblem
    
    Make
  - Feedback
  - Flags
  - Genarg
    
    ArgT
    
    GenObj
    
    Register
  - Hook
  - LStream
  - Loc
  - ObjFile
  - Pp
  - Pp_diff
    
    StringDiff
  - Rtree
    
    Smart
  - Spawn
    
    Control
    
    MainLoopModel
    
    Async
    
    Sync
  - Stateid
    
    Self
    
    Set
  - System
  - Util
    
    Empty
    
    String
    
    Set
    
    Map
    
    Smart
    
    Unsafe
    
    Monad
    
    Pred
    
    List
    
    List
    
    Smart
    
    MonoS
    
    Array
    
    Smart
    
    Fun1
    
    Smart
    
    Set
    
    OrderedType
    
    S
    
    Make
    
    HashedType
    
    Hashcons
    
    Map
    
    OrderedType
    
    MonadS
    
    S
    
    ExtS
    
    Set
    
    Smart
    
    Unsafe
    
    Monad
    
    Make
    
    Smart
    
    Unsafe
    
    Monad
    
    Union
  - Xml_datatype
- Library coq-core.library
  - Coqlib
  - Global
  - Globnames
    
    ExtRefOrdered
    
    ExtRefSet
    
    ExtRefMap
    
    Smart
    
    Unsafe
    
    Monad
  - Goptions
    
    MakeStringTable
    
    MakeRefTable
    
    OptionMap
  - Lib
  - Libnames
    
    Spmap
  - Libobject
    
    Dyn
    
    Map
    
    HMap
    
    Easy
  - Nametab
    
    GlobDirRef
    
    UnivIdMap
    
    Set
    
    Smart
    
    Unsafe
    
    Monad
    
    UserName
    
    EqualityType
    
    NAMETREE
    
    Make
  - Summary
    
    Dyn
    
    Map
    
    HMap
    
    Easy
    
    Local
- 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
  - Constr_matching
  - Detyping
    
    PrintingInductiveMake
    
    Set
  - Evarconv
  - Evardefine
  - Evarsolve
    
    AllowedEvars
  - Find_subterm
  - 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
    
    Unsafe
    
    Monad
  - Proof_diffs
- Library coq-core.proofs
  - Clenv
  - Evar_refiner
  - Goal
    
    V82
    
    Set
  - Goal_select
  - Logic
  - Miscprint
  - Proof
    
    V82
  - Proof_bullet
  - Refine
  - Tacmach
    
    Old
  - Tactypes
- Library coq-core.stm
  - AsyncTaskQueue
    
    Task
    
    MakeQueue
    
    MakeWorker
  - CoqworkmgrApi
  - 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
  - Coqargs
  - Coqinit
  - Coqloadpath
  - Usage
- Library coq-core.tactics
  - Abstract
  - Auto
  - Autorewrite
  - Btermdn
    
    Make
  - Cbn
  - Class_tactics
    
    Search
  - Contradiction
  - DeclareScheme
  - Dn
    
    Make
  - Dnet
    
    Datatype
    
    S
    
    Idset
    
    Make
    
    Idset
  - Eauto
  - Elim
  - Elimschemes
  - Eqdecide
  - Eqschemes
  - Equality
  - Genredexpr
  - Hints
    
    FullHint
    
    Hint_db
  - Hipattern
  - Ind_tables
  - Inv
  - Ppred
  - Redexpr
  - Redops
  - Tacticals
    
    Old
  - Tactics
    
    Simple
    
    New
  - Term_dnet
    
    IDENT
    
    OPT
    
    S
    
    Make
- Library coq-core.top_printers
  - Top_printers
- Library coq-core.toplevel
  - Ccompile
  - Coqc
  - Coqcargs
  - Coqloop
  - Coqrc
  - Coqtop
  - G_toplevel
    
    Toplevel_
  - Vernac
    
    State
  - WorkerLoop
- Library coq-core.vernac
  - Assumptions
  - Attributes
    
    Notations
  - Auto_ind_decl
  - Canonical
  - Classes
    
    Internal
  - ComArguments
  - ComAssumption
  - ComCoercion
  - ComDefinition
  - ComFixpoint
  - ComHints
  - ComInductive
  - ComPrimitive
  - ComProgramFixpoint
  - ComSearch
  - ComTactic
  - DebugHook
    
    Action
    
    Answer
    
    Intf
  - Declare
    
    Hook
    
    S
    
    CInfo
    
    Info
    
    OblState
    
    Proof
    
    Obls
    
    Internal
    
    Constant
  - DeclareInd
    
    Internal
  - DeclareUctx
  - DeclareUniv
  - Declaremods
  - Egramcoq
  - Egramml
  - Future
    
    UUID
    
    UUIDMap
    
    UUIDSet
  - G_proofs
    
    C
  - G_vernac
    
    C
  - Himsg
  - Indschemes
  - Library
  - Loadpath
  - Locality
  - Metasyntax
  - Mltop
  - Opaques
    
    Summary
  - Ppvernac
  - Prettyp
  - Printmod
  - Proof_using
  - Pvernac
    
    Vernac_
    
    Unsafe
  - RecLemmas
  - Record
    
    Ast
    
    Internal
  - RetrieveObl
  - Search
  - Topfmt
  - Vernac_classifier
  - Vernacentries
  - Vernacexpr
  - Vernacextend
    
    InProg
    
    OutProg
    
    InProof
    
    OutProof
  - Vernacinterp
  - Vernacprop
  - Vernacstate
    
    Parser
    
    System
    
    LemmaStack
    
    Stm
    
    Declare
- Library coq-core.vm
  - Coqrun
- Library coqide-server.core
  - Document
    
    signals
- Library coqide-server.protocol
  - Interface
  - Richpp
  - Serialize
  - Xml_lexer
  - Xml_parser
  - Xml_printer
  - Xmlprotocol
- 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
    
    CM
    
    History
    
    HP
    
    Unify
- Library funind_plugin
  - Funind_plugin
    
    Functional_principles_proofs
    
    Functional_principles_types
    
    G_indfun
    
    Vernac
    
    Tactic
    
    Gen_principle
    
    Glob_term_to_relation
    
    Glob_termops
    
    Indfun
    
    Indfun_common
    
    New
    
    Invfun
    
    Recdef
- Library ltac2_plugin
  - Ltac2_plugin
    
    G_ltac2
    
    Tac2core
    
    Core
    
    Tac2dyn
    
    Arg
    
    Param
    
    ArgMap
    
    Val
    
    Map
    
    HMap
    
    Easy
    
    Tac2entries
    
    Pltac
    
    Tac2env
    
    Tac2expr
    
    Tac2extffi
    
    Tac2ffi
    
    Valexpr
    
    Tac2intern
    
    Tac2interp
    
    Tac2match
    
    Tac2print
    
    Tac2qexpr
    
    Tac2quote
    
    Tac2stdlib
    
    Tac2tactics
    
    Tac2types
- Library ltac_plugin
  - Ltac_plugin
    
    Coretactics
    
    Evar_tactics
    
    Extraargs
    
    Extratactics
    
    G_auto
    
    G_class
    
    G_eqdecide
    
    G_ltac
    
    G_obligations
    
    Tactic
    
    G_rewrite
    
    G_tactic
    
    Internals
    
    Leminv
    
    Pltac
    
    Pptactic
    
    Profile_ltac
    
    Profile_ltac_tactics
    
    Rewrite
    
    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
    
    Mfourier
    
    IMap
    
    Fourier
    
    Proof
    
    Micromega
    
    Pos
    
    Coq_Pos
    
    N
    
    Z
    
    Mutils
    
    Int
    
    ISet
    
    IMap
    
    Cmp
    
    Tag
    
    TagSet
    
    CamlToCoq
    
    CoqToCaml
    
    Hash
    
    NumCompat
    
    ZArith
    
    QArith
    
    Z
    
    Notations
    
    Z
    
    Q
    
    Z
    
    Notations
    
    Persistent_cache
    
    PHashtable
    
    PHashtable
    
    Polynomial
    
    Mc
    
    Monomial
    
    MonMap
    
    Poly
    
    LinPoly
    
    MonT
    
    ProofFormat
    
    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
    
    Ssrprinters
    
    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
    
    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
    
    minisys.ml
    
    monad.ml
    
    neList.ml
    
    option.ml
    
    orderedType.ml
    
    predicate.ml
    
    range.ml
    
    segmenttree.ml
    
    store.ml
    
    terminal.ml
    
    trie.ml
    
    unicode.ml
    
    unicodetable.ml
    
    unionfind.ml
  - coq-core.config
    
    coq_config.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
    
    plexing.ml
  - coq-core.interp
    
    constrexpr.ml
    
    constrexpr_ops.ml
    
    constrextern.ml
    
    constrintern.ml
    
    decls.ml
    
    deprecation.ml
    
    dumpglob.ml
    
    genintern.ml
    
    impargs.ml
    
    implicit_quantifiers.ml
    
    modintern.ml
    
    notation.ml
    
    notation_ops.ml
    
    notation_term.ml
    
    numTok.ml
    
    reserve.ml
    
    smartlocate.ml
    
    stdarg.ml
    
    syntax_def.ml
  - coq-core.kernel
    
    cClosure.ml
    
    cPrimitives.ml
    
    constr.ml
    
    context.ml
    
    conv_oracle.ml
    
    cooking.ml
    
    declarations.ml
    
    declareops.ml
    
    entries.ml
    
    environ.ml
    
    esubst.ml
    
    evar.ml
    
    float64.ml
    
    float64_common.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
    
    term_typing.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
    
    dAst.ml
    
    envars.ml
    
    explore.ml
    
    feedback.ml
    
    flags.ml
    
    genarg.ml
    
    hook.ml
    
    lStream.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
    
    notation_gram.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
    
    geninterp.ml
    
    globEnv.ml
    
    glob_ops.ml
    
    glob_term.ml
    
    heads.ml
    
    indrec.ml
    
    inductiveops.ml
    
    keys.ml
    
    locus.ml
    
    locusops.ml
    
    ltac_pretype.ml
    
    nativenorm.ml
    
    pattern.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
    
    evar_refiner.ml
    
    goal.ml
    
    goal_select.ml
    
    logic.ml
    
    miscprint.ml
    
    proof.ml
    
    proof_bullet.ml
    
    refine.ml
    
    tacmach.ml
    
    tactypes.ml
  - coq-core.stm
    
    asyncTaskQueue.ml
    
    coqworkmgrApi.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
    
    usage.ml
  - coq-core.tactics
    
    abstract.ml
    
    auto.ml
    
    autorewrite.ml
    
    btermdn.ml
    
    cbn.ml
    
    class_tactics.ml
    
    contradiction.ml
    
    declareScheme.ml
    
    dn.ml
    
    dnet.ml
    
    eauto.ml
    
    elim.ml
    
    elimschemes.ml
    
    eqdecide.ml
    
    eqschemes.ml
    
    equality.ml
    
    genredexpr.ml
    
    hints.ml
    
    hipattern.ml
    
    ind_tables.ml
    
    inv.ml
    
    ppred.ml
    
    redexpr.ml
    
    redops.ml
    
    tacticals.ml
    
    tactics.ml
    
    term_dnet.ml
  - coq-core.top_printers
    
    top_printers.ml
  - coq-core.toplevel
    
    ccompile.ml
    
    coqc.ml
    
    coqcargs.ml
    
    coqloop.ml
    
    coqrc.ml
    
    coqtop.ml
    
    g_toplevel.ml
    
    vernac.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
    
    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
    
    topfmt.ml
    
    vernac_classifier.ml
    
    vernacentries.ml
    
    vernacexpr.ml
    
    vernacextend.ml
    
    vernacinterp.ml
    
    vernacprop.ml
    
    vernacstate.ml
  - coq-core.vm
    
    coqrun.ml
  - coqide-server.core
    
    document.ml
  - coqide-server.protocol
    
    interface.ml
    
    richpp.ml
    
    serialize.ml
    
    xml_lexer.ml
    
    xml_parser.ml
    
    xml_printer.ml
    
    xmlprotocol.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
    
    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
  - ltac_plugin
    
    coretactics.ml
    
    evar_tactics.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
    
    rewrite.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
    
    mfourier.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
    
    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 `Cbv`Source

Sourcetype cbv_infos

Entry point for cbv normalization of a constr

Source

val create_cbv_infos : 
  CClosure.RedFlags.reds ->
  Environ.env ->
  Evd.evar_map ->
  cbv_infos

Sourceval cbv_norm : cbv_infos -> EConstr.constr -> EConstr.constr

Sourcetype cbv_value =

| VAL of int * Constr.constr
| STACK of int * cbv_value * cbv_stack
| CBN of Constr.constr * cbv_value Esubst.subs
| LAM of int * (Names.Name.t Context.binder_annot * Constr.constr) list * Constr.constr * cbv_value Esubst.subs
| FIXP of Constr.fixpoint * cbv_value Esubst.subs * cbv_value array
| COFIXP of Constr.cofixpoint * cbv_value Esubst.subs * cbv_value array
| CONSTR of Names.constructor Univ.puniverses * cbv_value array
| PRIMITIVE of CPrimitives.t * Constr.pconstant * cbv_value array
| ARRAY of Univ.Instance.t * cbv_value Parray.t * cbv_value

Sourceand cbv_stack =

| TOP
| APP of cbv_value array * cbv_stack
| CASE of Univ.Instance.t * Constr.constr array * Constr.case_return * Constr.case_branch array * Constr.case_invert * Constr.case_info * cbv_value Esubst.subs * cbv_stack
| PROJ of Names.Projection.t * cbv_stack

Sourceval shift_value : int -> cbv_value -> cbv_value

Sourceval stack_app : cbv_value array -> cbv_stack -> cbv_stack

Sourceval strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack

Source

val cbv_stack_term : 
  cbv_infos ->
  cbv_stack ->
  cbv_value Esubst.subs ->
  Constr.constr ->
  cbv_value

recursive functions...

Source

val cbv_norm_term : 
  cbv_infos ->
  cbv_value Esubst.subs ->
  Constr.constr ->
  Constr.constr

Source

val norm_head : 
  cbv_infos ->
  cbv_value Esubst.subs ->
  Constr.constr ->
  cbv_stack ->
  cbv_value * cbv_stack

Sourceval apply_stack : cbv_infos -> Constr.constr -> cbv_stack -> Constr.constr

Sourceval cbv_norm_value : cbv_infos -> cbv_value -> Constr.constr

End of cbv debug section i

package coq

Module CbvSource

Module `Cbv`Source