package coq

You can search for identifiers within the package.

in-package search v0.2.0

coq-core.clib
- CArray
  - ExtS
    
    Floatarray
    
    Fun1
    
    Smart
    
    Smart
  - Floatarray
  - Fun1
    
    Smart
  - Smart
- CEphemeron
- CList
  - ExtS
    
    MonoS
    
    Smart
  - MonoS
  - Smart
- CMap
  - ExtS
    
    Monad
    
    M
    
    Set
    
    Smart
    
    Unsafe
  - MonadS
  - OrderedType
- CObj
- CPath
- CSet
  - Hashcons
    
    H
    
    M
  - HashedType
  - OrderedType
- CString
  - ExtS
    
    List
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - List
  - Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
- 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
    
    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
- 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
  - S
- Unicode
- Unicodetable
- Unionfind
  - Make
    
    M
    
    S
  - MapS
  - PartitionSig
  - SetS
coq-core.config
- Coq_config
coq-core.engine
- EConstr
  - EInstance
  - ESorts
  - Unsafe
  - Vars
- Evar_kinds
- Evarutil
- Evd
  - Abstraction
  - Filter
  - FutureGoals
  - Identity
  - Metamap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - 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
  - 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
- UnivGen
- UnivMinim
- UnivNames
- UnivProblem
  - Set
- UnivSubst
coq-core.gramlib
- Gramlib
  - Gramext
  - Grammar
    
    ExtS
    
    Entry
    
    Parsable
    
    Production
    
    Rule
    
    Rules
    
    Symbol
    
    Unsafe
    
    GMake
    
    Entry
    
    L
    
    State
    
    Parsable
    
    Production
    
    Rule
    
    Rules
    
    Symbol
    
    Unsafe
    
    S
    
    Entry
    
    Parsable
    
    Production
    
    Rule
    
    Rules
    
    Symbol
  - Plexing
    
    S
    
    State
coq-core.interp
- Constrexpr
- Constrexpr_ops
- Constrextern
- Constrintern
- Decls
- Deprecation
- Dumpglob
- Genintern
  - Store
- Impargs
- Implicit_quantifiers
- Modintern
- Notation
  - NotationMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - SpecificNotationMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
- Notation_ops
- Notation_term
- NumTok
  - Signed
  - SignedNat
  - Unsigned
  - UnsignedNat
- Reserve
- Smartlocate
- Stdarg
- Syntax_def
coq-core.kernel
- CClosure
  - RedFlags
  - RedFlagsSig
- CPrimitives
- Constr
- Context
  - Compacted
    
    Declaration
  - Named
    
    Declaration
  - Rel
    
    Declaration
- Conv_oracle
- Cooking
- Declarations
- Declareops
- Entries
- Environ
  - Globals
  - QConstant
  - QConstruct
  - QGlobRef
  - QInd
  - QMutInd
  - QNameS
  - QProjection
    
    Repr
- Esubst
  - Internal
- Evar
  - Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
- Float64
- Float64_common
- IndTyping
- Indtypes
- Inductive
- InferCumulativity
- Mod_subst
- Mod_typing
- Modops
- Names
  - Cmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Cmap_env
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Constant
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Constrmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Constrmap_env
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Construct
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Cpred
  - Cset
  - Cset_env
  - DPmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - DirPath
  - EqType
  - GlobRef
    
    CanOrd
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Map_env
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Set
    
    Set_env
    
    SyntacticOrd
    
    UserOrd
  - Id
    
    List
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Pred
  - Ind
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Indmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Indmap_env
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - KNmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - KNpred
  - KNset
  - KerName
  - Label
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - MBId
  - MBImap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - MPmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Mindmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Mindmap_env
    
    Monad
    
    M
    
    Set
    
    Smart
    
    Unsafe
  - Mindset
  - ModIdmap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - 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
- Parray
- Primred
  - RedNative
    
    E
  - RedNativeEntries
- Reduction
- Relevanceops
- Retroknowledge
- Safe_typing
- Section
- Sorts
- Subtyping
- Term
- Term_typing
- TransparentState
- Type_errors
- Typeops
- UGraph
  - Bound
- Uint63
- Univ
  - AUContext
  - Constraint
  - ContextSet
  - Instance
  - LMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - LSet
  - Level
    
    UGlobal
  - UContext
  - Universe
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Variance
- Vars
- Vconv
- Vm
- Vmbytecodes
  - Label
- Vmbytegen
- Vmemitcodes
- Vmlambda
- Vmopcodes
- Vmsymtable
- Vmvalues
coq-core.lib
- AcyclicGraph
  - Make
    
    Point
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Set
  - Point
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
    
    Set
- Aux_file
- CAst
- CDebug
- CErrors
- CProfile
- CWarnings
- Control
- CoqProject_file
- DAst
- Envars
- Explore
  - Make
    
    S
  - SearchProblem
- Feedback
- Flags
- Future
  - UUID
- Genarg
  - ArgT
  - GenObj
  - Register
    
    M
- Hook
- LStream
- Loc
- ObjFile
- Pp
- Pp_diff
  - StringDiff
- Rtree
  - Smart
- Spawn
  - Async
    
    ML
  - Control
  - MainLoopModel
  - Sync
- Stateid
- System
- Util
  - Array
    
    Floatarray
    
    Fun1
    
    Smart
    
    Smart
  - Empty
  - List
    
    MonoS
    
    Smart
  - Map
    
    ExtS
    
    Monad
    
    M
    
    Set
    
    Smart
    
    Unsafe
    
    MonadS
    
    OrderedType
  - Set
    
    Hashcons
    
    H
    
    M
    
    HashedType
    
    OrderedType
  - String
    
    List
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - Union
coq-core.library
- Coqlib
- Global
- Globnames
  - ExtRefMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
  - ExtRefOrdered
  - ExtRefSet
- Goptions
  - MakeRefTable
    
    A
    
    Set
  - MakeStringTable
    
    A
  - OptionMap
- Lib
- Libnames
  - Spmap
- Libobject
  - Dyn
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
- Nametab
  - EqualityType
  - GlobDirRef
  - Make
    
    E
    
    U
  - NAMETREE
  - UnivIdMap
    
    Monad
    
    M
    
    Set
    
    Smart
    
    Unsafe
  - UserName
- Summary
  - Dyn
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
  - Local
coq-core.parsing
- CLexer
  - Error
  - Lexer
    
    State
  - LexerDiff
    
    State
- Extend
- G_constr
- G_prim
- Notation_gram
- Notgram_ops
- Pcoq
  - Constr
  - Entry
  - GramState
  - Lookahead
  - Module
  - Parsable
  - Prim
  - Production
  - Rule
  - Rules
  - Symbol
- Ppextend
- Tok
coq-core.plugins.btauto
- Btauto_plugin
  - G_btauto
  - Refl_btauto
    
    Btauto
coq-core.plugins.cc
- Cc_plugin
  - Ccalgo
    
    PacMap
    
    PafMap
  - Ccproof
  - Cctac
  - G_congruence
coq-core.plugins.derive
- Derive_plugin
  - Derive
  - G_derive
coq-core.plugins.extraction
- Extraction_plugin
  - Big
  - 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
    
    CM
    
    HP
  - Unify
coq-core.plugins.float_syntax
- Float_syntax_plugin
  - Float_syntax
coq-core.plugins.funind
- Funind_plugin
coq-core.plugins.ltac
- Ltac_plugin
  - Coretactics
  - Evar_tactics
  - Extraargs
  - Extratactics
  - G_auto
  - G_class
  - G_eqdecide
  - G_ltac
  - G_obligations
  - G_rewrite
  - G_tactic
  - Leminv
  - Pltac
  - Pptactic
  - Profile_ltac
  - Profile_ltac_tactics
  - Rewrite
  - 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
  - Tac2core
    
    Core
  - Tac2dyn
    
    Arg
    
    ArgMap
    
    M
    
    Param
    
    Val
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
  - Tac2entries
    
    Pltac
  - Tac2env
  - Tac2expr
  - Tac2extffi
  - Tac2ffi
    
    Valexpr
  - Tac2intern
  - Tac2interp
  - Tac2match
  - Tac2print
  - Tac2qexpr
  - Tac2quote
  - Tac2stdlib
  - Tac2tactics
  - Tac2types
coq-core.plugins.micromega
- Micromega_plugin
  - Certificate
  - Coq_micromega
  - G_micromega
  - Itv
  - Mfourier
    
    Fourier
    
    IMap
    
    Proof
  - Micromega
    
    Coq_Pos
    
    N
    
    Pos
    
    Z
  - Mutils
    
    CamlToCoq
    
    Cmp
    
    CoqToCaml
    
    Hash
    
    IMap
    
    ISet
    
    Int
    
    Tag
    
    TagSet
  - NumCompat
    
    Q
    
    Notations
    
    QArith
    
    Notations
    
    Z
    
    Z
    
    ZArith
  - Persistent_cache
    
    PHashtable
  - Polynomial
    
    BoundWithProof
    
    LinPoly
    
    MonT
    
    MonMap
    
    Monomial
    
    Poly
    
    ProofFormat
    
    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
  - Ssrprinters
  - Ssrtacticals
  - Ssrvernac
  - Ssrview
    
    AdaptorDb
coq-core.plugins.ssrmatching
- Ssrmatching_plugin
  - G_ssrmatching
  - Ssrmatching
    
    Internal
coq-core.plugins.ssrsearch
- Ssrsearch_plugin
  - G_search
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
- Geninterp
  - TacStore
  - Val
  - ValTMap
    
    Value
- GlobEnv
- Glob_ops
- Glob_term
- Heads
- Indrec
- Inductiveops
- Keys
- Locus
- Locusops
- Ltac_pretype
- Nativenorm
- Pattern
- Patternops
- Pretype_errors
- Pretyping
- Program
- Reductionops
- Retyping
- Structures
- Tacred
- Typeclasses
- Typeclasses_errors
- Typing
- Unification
- Vnorm
coq-core.printing
- Genprint
- Ppconstr
- Pputils
- Printer
  - ContextObjectMap
    
    Monad
    
    M
    
    Smart
    
    Unsafe
- Proof_diffs
coq-core.proofs
- Clenv
- Evar_refiner
- Goal
  - V82
- Goal_select
- Logic
- Miscprint
- Proof
  - V82
- Proof_bullet
- Refine
- Tacmach
  - New
- Tactypes
coq-core.stm
- AsyncTaskQueue
  - MakeQueue
    
    T
  - MakeWorker
    
    T
  - Task
- CoqworkmgrApi
- Dag
  - Make
    
    Property
  - S
    
    Property
- Partac
  - TacTask
- ProofBlockDelimiter
- Spawned
- Stm
  - AsyncOpts
  - DynBlockData
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
  - ProofTask
  - QueryTask
- Stmargs
- TQueue
- Vcs
  - Make
    
    Branch
    
    Dag
    
    Property
  - S
    
    Branch
    
    Dag
    
    Property
- Vio_checking
- WorkerPool
  - Make
    
    Model
  - PoolModel
coq-core.sysinit
- Coqargs
- Coqinit
- Coqloadpath
- Usage
coq-core.tactics
- Abstract
- Auto
- Autorewrite
- Btermdn
  - Make
- Cbn
- Class_tactics
  - Search
- Contradiction
- DeclareScheme
- DeclareUctx
- Dn
  - Make
- Dnet
  - Datatype
  - Make
    
    T
  - S
- Eauto
- Elim
- Elimschemes
- Eqdecide
- Eqschemes
- Equality
- Genredexpr
- Hints
  - FullHint
  - Hint_db
- Hipattern
- Ind_tables
- Inv
- Ppred
- Redexpr
- Redops
- Tacticals
  - New
- Tactics
  - New
  - Simple
- Term_dnet
  - IDENT
  - Make
    
    Ident
    
    Opt
  - OPT
  - S
coq-core.top_printers
- Top_printers
coq-core.toplevel
- Ccompile
- Coqc
- Coqcargs
- Coqloop
- Coqrc
- Coqtop
- G_toplevel
  - Toplevel_
- Vernac
  - State
- WorkerLoop
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
  - CInfo
  - Hook
    
    S
  - Info
  - Internal
    
    Constant
  - OblState
  - Obls
  - Proof
- DeclareInd
  - Internal
- DeclareUniv
- Declaremods
- Egramcoq
- Egramml
- G_proofs
- G_vernac
- Himsg
- Indschemes
- Library
- Loadpath
- Locality
- Metasyntax
- Mltop
- Ppvernac
- Prettyp
- Printmod
- Proof_using
- Pvernac
  - Unsafe
  - Vernac_
- RecLemmas
- Record
  - Ast
  - Internal
- RetrieveObl
- Search
- Topfmt
- Vernac_classifier
- Vernacentries
- Vernacexpr
- Vernacextend
- Vernacinterp
- Vernacprop
- Vernacstate
  - Declare
  - LemmaStack
  - Parser
  - Stm
  - System
coq-core.vm
- Coqrun
coqide-server.core
- Document
  - signals
coqide-server.protocol
- Interface
- Richpp
- Serialize
- Xml_lexer
- Xml_parser
- Xml_printer
- Xmlprotocol

Legend:
Library
Module
Module type
Parameter
Class
Class type

val typecheck_inductive : 
  Environ.env ->
  sec_univs:Univ.Level.t array option ->
  Entries.mutual_inductive_entry ->
  Environ.env
  * Declarations.universes
  * Declarations.template_universes option
  * Univ.Variance.t array option
  * Names.Id.t array option option
  * Constr.rel_context
  * ((Declarations.inductive_arity * Constr.types array)
     * (Constr.rel_context * (Constr.rel_context * Constr.types) array)
     * Sorts.family)
      array

Type checking for some inductive entry. Returns:

environment with inductives + parameters in rel context
abstracted universes
checked variance info (variance for section universes is at the beginning of the array)
record entry (checked to be OK)
parameters
for each inductive, (arity * constructors) (with params) * (indices * splayed constructor types) (both without params) * top allowed elimination

val template_polymorphic_univs : 
  ctor_levels:Univ.LSet.t ->
  Univ.ContextSet.t ->
  Constr.rel_context ->
  Univ.Universe.t ->
  (Univ.LSet.t * Univ.Level.t option list) option