package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

rocq-runtime
- README
- Library btauto_plugin
  - Btauto_plugin
    
    G_btauto
    
    Refl_btauto
    
    Btauto
- Library byte_config
  - Coq_byte_config
- Library cc_core_plugin
  - Cc_core_plugin
    
    Ccalgo
    
    ATerm
    
    Ccprojectability
    
    Ccproof
    
    Cctac
- Library cc_plugin
  - Cc_plugin
    
    G_congruence
- Library derive_plugin
  - Derive_plugin
    
    Derive
    
    G_derive
- Library extraction_plugin
  - Extraction_plugin
    
    Common
    
    State
    
    Extract_env
    
    Extraction
    
    G_extraction
    
    Haskell
    
    Json
    
    Miniml
    
    InfvInst
    
    Mlutil
    
    Mlenv
    
    Modutil
    
    Ocaml
    
    Scheme
    
    Table
    
    Refset'
    
    Refmap'
- Library firstorder_core_plugin
  - Firstorder_core_plugin
    
    Formula
    
    Env
    
    Ground
    
    Instances
    
    Rules
    
    Sequent
    
    Unify
    
    Item
- Library firstorder_plugin
  - Firstorder_plugin
    
    G_ground
- 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_ltac1_plugin
  - Ltac2_ltac1_plugin
    
    G_ltac2_ltac1
    
    Tac2core_ltac1
    
    Tac2quote_ltac1
    
    Tac2stdlib_ltac1
- Library ltac2_plugin
  - Ltac2_plugin
    
    G_ltac2
    
    Tac2bt
    
    Tac2core
    
    MapType
    
    S
    
    M
    
    Smart
    
    Monad
    
    Tac2dyn
    
    Arg
    
    Param
    
    ArgMap
    
    Val
    
    Map
    
    HMap
    
    Easy
    
    Tac2entries
    
    Tac2Custom
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    Pred
    
    CustomTab
    
    Pltac
    
    Tac2env
    
    Tac2expr
    
    PartialPat
    
    Tac2externals
    
    Tac2extffi
    
    Tac2extravals
    
    Tac2ffi
    
    ModField
    
    Tac2intern
    
    Tac2interp
    
    Tac2match
    
    Tac2print
    
    Tac2qexpr
    
    Tac2quote
    
    Refs
    
    Tac2stdlib
    
    Tac2tactics
    
    RewriteStrats
    
    Tac2types
    
    Tac2typing_env
    
    TVar
    
    Map
    
    Tac2val
    
    Valexpr
- Library ltac_plugin
  - Ltac_plugin
    
    ComRewrite
    
    Coretactics
    
    Extraargs
    
    Extratactics
    
    G_auto
    
    G_class
    
    G_eqdecide
    
    G_ltac
    
    G_rewrite
    
    G_tactic
    
    Internals
    
    Leminv
    
    Pltac
    
    Pptactic
    
    Profile_ltac_tactics
    
    Tacarg
    
    Taccoerce
    
    Value
    
    Tacentries
    
    Tacenv
    
    Tacexpr
    
    Tacintern
    
    Tacinterp
    
    Value
    
    TacStore
    
    Tacsubst
    
    Tactic_debug
    
    Tactic_matching
- Library micromega_core_plugin
  - Micromega_core_plugin
    
    Micromega
    
    Pos
    
    Coq_Pos
    
    N
    
    Z
    
    Mutils
    
    ISet
    
    IMap
    
    Smart
    
    Monad
    
    Cmp
    
    Tag
    
    TagSet
    
    McPrinter
    
    Mc
    
    CamlToCoq
    
    CoqToCaml
    
    Hash
    
    NumCompat
    
    ZArith
    
    QArith
    
    Z
    
    Notations
    
    Z
    
    Q
    
    Z
    
    Notations
    
    Sos
    
    Sos_lib
    
    Sos_types
- Library micromega_plugin
  - Micromega_plugin
    
    Certificate
    
    Mc
    
    Coq_micromega
    
    G_micromega
    
    Itv
    
    Linsolve
    
    Persistent_cache
    
    PHashtable
    
    PHashtable
    
    Polynomial
    
    Mc
    
    Monomial
    
    MonMap
    
    Poly
    
    LinPoly
    
    MonT
    
    ProofFormat
    
    Env
    
    WithProof
    
    BoundWithProof
    
    Simplex
    
    Vect
    
    Bound
- Library nsatz_core_plugin
  - Nsatz_core_plugin
    
    Ideal
    
    Monomial
    
    Make
    
    Hashpol
    
    Nsatz
    
    Polynom
    
    Coef
    
    S
    
    Hashpol
    
    Make
    
    Hashpol
    
    Utile
- Library nsatz_plugin
  - Nsatz_plugin
    
    G_nsatz
- Library number_string_notation_plugin
  - Number_string_notation_plugin
    
    G_number_string
    
    Number_string
- Library ring_plugin
  - Ring_plugin
    
    G_ring
    
    Ring
    
    Ring_ast
- Library rocq-runtime.boot
  - Boot
    
    Env
    
    Path
    
    Path
    
    Usage
    
    Util
- Library rocq-runtime.checklib
  - Coq_checklib
    
    Analyze
    
    LargeArray
    
    Input
    
    S
    
    Make
    
    CheckFlags
    
    CheckInductive
    
    CheckLibrary
    
    Check_stat
    
    Coqchk_main
    
    Mod_checking
    
    Safe_checking
    
    Validate
    
    Values
- Library rocq-runtime.clib
  - CArray
    
    S
    
    Smart
    
    Fun1
    
    Smart
  - CEphemeron
  - CList
    
    Smart
    
    MonoS
  - CMap
    
    OrderedType
    
    MonadS
    
    S
    
    UExtS
    
    Set
    
    Smart
    
    Monad
    
    ExtS
    
    Set
    
    Smart
    
    Monad
    
    Make
    
    Smart
    
    Monad
  - CObj
  - CSet
    
    OrderedType
    
    S
    
    ExtS
    
    List
    
    Make
    
    List
    
    HashedType
    
    Hashcons
  - CSig
    
    USetS
    
    SetS
    
    UMapS
    
    MapS
  - CString
    
    S
    
    Set
    
    List
    
    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
    
    HashconsedRecType
    
    S
    
    Make
    
    MakeRec
    
    HashedType
    
    Hlist
  - Hashset
    
    EqType
    
    S
    
    Make
    
    Combine
  - Heap
    
    Ordered
    
    S
    
    Functional
  - IStream
  - Int
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    List
    
    PArray
    
    PMap
  - Memprof_coq
    
    Masking
    
    Thread_map
    
    Resource_bind
    
    Mutex_aux
  - Monad
    
    Def
    
    ListS
    
    S
    
    List
    
    Make
    
    List
  - Mutex_aux
  - 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
  - WriteOnceArray
    
    Internal
- Library rocq-runtime.config
  - Coq_config
- Library rocq-runtime.coqargs
  - Coqargs
- Library rocq-runtime.coqdeplib
  - Coqdeplib
    
    Args
    
    Common
    
    State
    
    Dep_info
    
    Dep
    
    Set
    
    List
    
    Error
    
    File_util
    
    Fl
    
    Internal
    
    Lexer
    
    Loadpath
    
    Filename
    
    FileSet
    
    State
    
    Makefile
    
    Rocqdep_main
- Library rocq-runtime.coqworkmgrapi
  - CoqworkmgrApi
- Library rocq-runtime.debugger_support
  - Debugger_support
- Library rocq-runtime.dev
  - Top_printers
  - Vm_printers
- Library rocq-runtime.engine
  - EConstr
    
    ERelevance
    
    ESorts
    
    EInstance
    
    UnsafeMonomorphic
    
    Vars
    
    Unsafe
    
    Expand
  - Evar_kinds
  - Evarnames
  - Evarutil
    
    VarSet
  - Evd
    
    Filter
    
    Abstraction
    
    FutureGoals
    
    Store
    
    MonadR
    
    List
    
    Monad
    
    List
    
    MiniEConstr
    
    ERelevance
    
    ESorts
    
    EInstance
    
    Expand
  - Ftactic
    
    List
    
    Notations
  - Logic_monad
    
    NonLogical
    
    List
    
    BackState
    
    Param
    
    Logical
    
    List
    
    Unsafe
  - Namegen
    
    Generator
  - Nameops
    
    Subscript
    
    Fresh
    
    Name
  - PolyFlags
  - Profile_tactic
  - 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
  - UnivFlex
  - UnivGen
    
    QualityOrSet
  - UnivMinim
    
    UPairSet
  - UnivNames
  - UnivProblem
    
    Set
  - UnivSubst
- Library rocq-runtime.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 rocq-runtime.interp
  - Abbreviation
  - Constrexpr
  - Constrexpr_ops
  - Constrextern
  - Constrintern
    
    Interner
  - Decls
  - Dumpglob
  - Genintern
    
    Store
  - Impargs
  - Implicit_quantifiers
  - Modintern
  - Notation
    
    NotationSet
    
    List
    
    NotationMap
    
    Smart
    
    Monad
    
    SpecificNotationSet
    
    List
    
    SpecificNotationMap
    
    Smart
    
    Monad
  - Notation_ops
  - Notation_term
  - Notationextern
  - NumTok
    
    UnsignedNat
    
    SignedNat
    
    Unsigned
    
    Signed
  - PrimNotations
  - Reserve
  - Smartlocate
- Library rocq-runtime.kernel
  - CClosure
  - CPrimitives
  - Constant_typing
  - Constr
    
    UnsafeMonomorphic
    
    GenHCons
  - Context
    
    Rel
    
    Declaration
    
    Named
    
    Declaration
    
    Compacted
    
    Declaration
  - Conv_oracle
  - Conversion
  - Cooking
  - Declarations
  - Declareops
  - Discharge
  - Entries
  - Environ
    
    QS
    
    QMapS
    
    QMap
    
    QNameS
    
    QConstant
    
    Map
    
    QMutInd
    
    Map
    
    QInd
    
    Map
    
    QConstruct
    
    Map
    
    QProjection
    
    Map
    
    Repr
    
    Map
    
    QGlobRef
    
    Map
    
    Internal
    
    View
  - Esubst
    
    Internal
  - Evar
    
    Set
    
    Map
    
    Smart
    
    Monad
  - Float64
  - Float64_common
  - Genlambda
    
    S
    
    Make
  - HConstr
    
    Tbl
  - IndTyping
    
    NotPrimRecordReason
  - Indtypes
  - Inductive
    
    Template
  - InferCumulativity
  - Mod_declarations
  - Mod_subst
  - Mod_typing
  - Modops
  - Names
    
    Id
    
    Set
    
    List
    
    Map
    
    Smart
    
    Monad
    
    Pred
    
    List
    
    Name
    
    DirPath
    
    Set
    
    List
    
    Map
    
    Smart
    
    Monad
    
    DPset
    
    DPmap
    
    MBId
    
    Set
    
    List
    
    Map
    
    Smart
    
    Monad
    
    MBIset
    
    MBImap
    
    ModPath
    
    Set
    
    List
    
    Map
    
    Smart
    
    Monad
    
    MPset
    
    MPmap
    
    KerName
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    Pred
    
    KNset
    
    KNpred
    
    KNmap
    
    EqType
    
    QNameS
    
    CanOrd
    
    UserOrd
    
    Constant
    
    CanOrd
    
    UserOrd
    
    Cpred
    
    Cset
    
    Cset_env
    
    Cmap
    
    Smart
    
    Monad
    
    Cmap_env
    
    Smart
    
    Monad
    
    MutInd
    
    CanOrd
    
    UserOrd
    
    Mindset
    
    Mindmap
    
    Smart
    
    Monad
    
    Mindmap_env
    
    Set
    
    Smart
    
    Monad
    
    Ind
    
    CanOrd
    
    UserOrd
    
    Construct
    
    CanOrd
    
    UserOrd
    
    Indset
    
    List
    
    Constrset
    
    List
    
    Indset_env
    
    List
    
    Constrset_env
    
    List
    
    Indmap
    
    Smart
    
    Monad
    
    Constrmap
    
    Smart
    
    Monad
    
    Indmap_env
    
    Smart
    
    Monad
    
    Constrmap_env
    
    Smart
    
    Monad
    
    Projection
    
    Repr
    
    CanOrd
    
    UserOrd
    
    CanOrd
    
    UserOrd
    
    PRset
    
    PRmap
    
    Smart
    
    Monad
    
    PRpred
    
    GlobRef
    
    CanOrd
    
    UserOrd
    
    Set_env
    
    Map_env
    
    Smart
    
    Monad
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    Label
    
    Set
    
    List
    
    Map
    
    Smart
    
    Monad
  - Nativecode
  - Nativeconv
  - Nativelambda
  - Nativelib
  - Nativelibrary
  - Nativevalues
  - Opaqueproof
    
    HandleMap
  - PConstraints
  - Parray
  - Partial_subst
  - Primred
    
    RedNativeEntries
    
    RedNative
    
    RedNative
  - Pstring
  - QGraph
    
    ElimTable
  - RedFlags
  - Reduction
  - Relevanceops
  - Retroknowledge
  - Rtree
    
    Smart
    
    Kind
  - Safe_typing
  - Section
  - Sorts
    
    QGlobal
    
    QVar
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    Quality
    
    Constants
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    ElimConstraint
    
    ElimConstraints
    
    QContextSet
  - Subtyping
  - Term
  - TransparentState
  - Type_errors
  - Typeops
  - UGraph
    
    Internal
  - UVars
    
    Variance
    
    Instance
    
    QPairSet
    
    UContext
    
    AbstractContext
  - Uint63
  - Univ
    
    UGlobal
    
    Level
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    Universe
    
    Set
    
    List
    
    Map
    
    Smart
    
    Monad
    
    UnivConstraint
    
    UnivConstraints
    
    List
    
    ContextSet
  - Values
  - Vars
  - Vconv
  - Vm
  - Vmbytecodes
    
    Label
  - Vmbytegen
  - Vmemitcodes
  - Vmerrors
  - Vmlambda
  - Vmlibrary
  - Vmopcodes
  - Vmsymtable
  - Vmvalues
- Library rocq-runtime.lib
  - AcyclicGraph
    
    Point
    
    Set
    
    Map
    
    Smart
    
    Monad
    
    Make
  - Aux_file
    
    H
    
    M
  - CAst
    
    Smart
  - CDebug
  - CErrors
  - CWarnings
    
    CoreCategories
  - Control
  - CoqProject_file
  - DAst
  - Deprecation
    
    Version
  - Envars
  - Feedback
  - Flags
  - Hook
  - Instr
  - Loc
  - NewProfile
    
    MiniJson
    
    Counters
  - ObjFile
  - Pp
  - Pp_diff
    
    StringDiff
  - Quickfix
  - Spawn
    
    Control
    
    MainLoopModel
    
    Async
    
    Sync
  - Stateid
    
    Self
    
    Set
  - System
  - UserWarn
  - Util
    
    Empty
    
    String
    
    List
    
    Array
    
    Set
    
    Map
    
    Union
    
    Compare
  - Xml_datatype
- Library rocq-runtime.library
  - Coqlib
  - Global
    
    Internal
  - Globnames
    
    ExtRefOrdered
    
    ExtRefSet
    
    ExtRefMap
    
    Smart
    
    Monad
    
    CustomName
  - Goptions
    
    MakeStringTable
    
    RefConvertArg
    
    Set
    
    MakeRefTable
    
    OptionMap
  - Lib
    
    StagedLibS
    
    Synterp
    
    Interp
  - Libnames
    
    Spmap
  - Libobject
    
    Dyn
    
    Map
    
    HMap
    
    Easy
    
    ExportObj
  - Library_info
  - Locality
  - Nametab
    
    GlobDirRef
    
    NAMETAB
    
    WarnedTab
    
    XRefs
    
    Univs
    
    Quality
    
    ModTypes
    
    Modules
    
    OpenMods
    
    CustomEntries
    
    ValueType
    
    Map
    
    StateInfo
    
    EasyNoWarn
    
    WarnInfo
    
    Map
    
    MakeWarned
    
    SimpleWarnS
    
    Easy
  - Rocqlib
  - Summary
    
    Stage
    
    Dyn
    
    Map
    
    HMap
    
    Easy
    
    FrozenStage
    
    Synterp
    
    Interp
    
    OBSERVABLE
    
    OBSERVABLE_USER
    
    MakeObservable
- Library rocq-runtime.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
  - Procq
    
    Parsable
    
    Entry
    
    Symbol
    
    Rule
    
    Rules
    
    Production
    
    Lookahead
    
    Prim
    
    Constr
    
    Module
    
    GramState
  - Tok
- Library rocq-runtime.perf
  - Perf
- Library rocq-runtime.pretyping
  - Arguments_renaming
  - Cases
  - Cbv
  - Coercion
  - Coercionops
    
    ClTypSet
    
    List
  - Combinators
  - Constr_matching
  - Detyping
  - Evaluable
  - Evarconv
  - Evardefine
  - Evarsolve
    
    AllowedEvars
  - Find_subterm
  - Genarg
    
    ArgT
    
    GenObj
    
    Register
  - Geninterp
    
    Val
    
    ValTMap
    
    TacStore
  - Gensubst
  - GlobEnv
  - Glob_ops
  - Glob_term
  - Heads
  - Inductiveops
    
    Internal
  - Keys
  - LibBinding
    
    State
  - Locus
  - Locusops
  - Ltac_pretype
  - Nativenorm
  - Pattern
  - Patternops
  - Pretype_errors
  - Pretyping
  - PrintingFlags
    
    Detype
    
    Extern
    
    FactorizeEqns
    
    Records
    
    PrintingInductiveMake
    
    Set
  - Program
  - Reductionops
    
    CredNative
    
    ReductionBehaviour
    
    Db
    
    Stack
  - Retyping
  - Structures
    
    Structure
    
    Instance
    
    ValuePattern
    
    CanonicalSolution
    
    CSTable
    
    PrimitiveProjections
  - Tacred
  - TemplateArity
  - Typeclasses
  - Typeclasses_errors
  - Typing
  - Unification
    
    Metaset
    
    Metamap
    
    Smart
    
    Monad
    
    Meta
  - Vnorm
- Library rocq-runtime.printing
  - Genprint
  - Ppconstr
  - Ppextend
  - Pputils
  - Printer
    
    ContextObjectSet
    
    List
    
    ContextObjectMap
    
    Smart
    
    Monad
    
    Debug
  - Proof_diffs
- Library rocq-runtime.proofs
  - Clenv
    
    Internal
  - Goal_select
  - Logic
  - Miscprint
  - Proof
  - Proof_bullet
  - Refine
  - Subproof
  - Tacmach
  - Tactypes
- Library rocq-runtime.rocqshim
  - Rocqshim
- Library rocq-runtime.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
  - WorkerPool
    
    PoolModel
    
    Make
- Library rocq-runtime.sysinit
  - Coqinit
  - Coqloadpath
- Library rocq-runtime.tactics
  - Abstract
  - AllScheme
  - Auto
  - Autorewrite
    
    RewRule
  - Btermdn
    
    Make
  - Cbn
  - Class_tactics
    
    Search
  - Contradiction
  - DeclareScheme
  - Dn
    
    Make
  - EClause
  - Eauto
  - Elim
  - Elimschemes
  - Eqdecide
  - Eqschemes
  - Equality
  - Evar_tactics
  - FixTactics
  - Generalize
  - Genredexpr
  - Gentactic
  - Hints
    
    FullHint
    
    Modes
    
    Hint_db
  - Hipattern
  - Ind_tables
    
    Locmap
  - Indrec
  - Induction
  - Inv
  - Ppred
  - Redexpr
    
    Intern
    
    Interp
    
    User
  - Redops
  - Rewrite
    
    Strategies
    
    Internal
  - Stdarg
  - TacticErrors
  - Tacticals
  - Tactics
    
    Simple
    
    Internal
- Library rocq-runtime.toplevel
  - Ccompile
  - Colors
  - Common_compile
  - Coqc
  - Coqcargs
  - Coqloop
  - Coqrc
  - Coqtop
  - G_toplevel
  - Load
  - Memtrace_init
  - Vernac
    
    State
  - WorkerLoop
- Library rocq-runtime.vernac
  - Assumptions
  - Attributes
    
    Notations
  - Auto_ind_decl
  - Canonical
  - Classes
    
    Event
    
    Internal
  - ComArguments
  - ComAssumption
  - ComCoercion
  - ComDefinition
  - ComExtraDeps
  - ComFixpoint
  - ComHints
  - ComInductive
    
    Mind_decl
    
    Internal
  - ComPrimitive
  - ComRewriteRule
  - ComSearch
  - ComTactic
  - DebugHook
    
    Action
    
    Answer
    
    Intf
  - Declare
    
    Hook
    
    S
    
    CInfo
    
    Info
    
    OblState
    
    View
    
    Obl
    
    Proof
    
    Obls
    
    Internal
    
    Constant
  - DeclareInd
    
    Internal
  - DeclareUniv
  - Declaremods
    
    Synterp
    
    Interp
  - Egramml
  - Egramrocq
  - Future
    
    UUID
    
    UUIDMap
    
    UUIDSet
  - G_obligations
  - G_proofs
  - G_redexpr
  - G_vernac
  - Himsg
  - Indschemes
    
    Internal
  - Library
    
    Intern
    
    Provenance
  - Loadpath
    
    Error
  - Metasyntax
  - Mltop
    
    PluginSpec
  - Opaques
    
    Summary
  - Ppvernac
  - Prettyp
  - Printmod
  - Proof_using
  - Pvernac
    
    Vernac_
    
    Unsafe
  - RecLemmas
  - Record
    
    Data
    
    Ast
    
    RecordEntry
    
    Record_decl
    
    Internal
  - RetrieveObl
  - Search
  - Synterp
  - Tactic_option
  - Topfmt
  - VernacControl
  - Vernac_classifier
  - Vernacentries
    
    Preprocessed_Mind_decl
    
    DefAttributes
    
    Observer
  - Vernacexpr
  - Vernacextend
  - Vernacinterp
  - Vernacoptions
  - Vernacprop
  - Vernacstate
    
    Synterp
    
    System
    
    LemmaStack
    
    Interp
    
    System
    
    Stm
    
    Declare
  - Vernactypes
    
    Prog
    
    Proof
    
    OpaqueAccess
- Library rocq-runtime.vm
  - Coqrun
- 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 tuto4_plugin
  - Tuto4_plugin
    
    Myexternals
- 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
  - byte_config
    
    coq_byte_config.ml
  - cc_core_plugin
    
    cc_core_plugin.ml
    
    ccalgo.ml
    
    ccprojectability.ml
    
    ccproof.ml
    
    cctac.ml
  - cc_plugin
    
    cc_plugin.ml
    
    g_congruence.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_core_plugin
    
    firstorder_core_plugin.ml
    
    formula.ml
    
    ground.ml
    
    instances.ml
    
    rules.ml
    
    sequent.ml
    
    unify.ml
  - firstorder_plugin
    
    firstorder_plugin.ml
    
    g_ground.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_ltac1_plugin
    
    g_ltac2_ltac1.ml
    
    ltac2_ltac1_plugin.ml
    
    tac2core_ltac1.ml
    
    tac2quote_ltac1.ml
    
    tac2stdlib_ltac1.ml
  - ltac2_plugin
    
    g_ltac2.ml
    
    ltac2_plugin.ml
    
    tac2bt.ml
    
    tac2core.ml
    
    tac2dyn.ml
    
    tac2entries.ml
    
    tac2env.ml
    
    tac2externals.ml
    
    tac2extffi.ml
    
    tac2extravals.ml
    
    tac2ffi.ml
    
    tac2intern.ml
    
    tac2interp.ml
    
    tac2match.ml
    
    tac2print.ml
    
    tac2quote.ml
    
    tac2stdlib.ml
    
    tac2tactics.ml
    
    tac2typing_env.ml
    
    tac2val.ml
  - ltac_plugin
    
    comRewrite.ml
    
    coretactics.ml
    
    extraargs.ml
    
    extratactics.ml
    
    g_auto.ml
    
    g_class.ml
    
    g_eqdecide.ml
    
    g_ltac.ml
    
    g_rewrite.ml
    
    g_tactic.ml
    
    internals.ml
    
    leminv.ml
    
    ltac_plugin.ml
    
    pltac.ml
    
    pptactic.ml
    
    profile_ltac_tactics.ml
    
    tacarg.ml
    
    taccoerce.ml
    
    tacentries.ml
    
    tacenv.ml
    
    tacintern.ml
    
    tacinterp.ml
    
    tacsubst.ml
    
    tactic_debug.ml
    
    tactic_matching.ml
  - micromega_core_plugin
    
    micromega.ml
    
    micromega_core_plugin.ml
    
    mutils.ml
    
    numCompat.ml
    
    sos.ml
    
    sos_lib.ml
    
    sos_types.ml
  - micromega_plugin
    
    certificate.ml
    
    coq_micromega.ml
    
    g_micromega.ml
    
    itv.ml
    
    linsolve.ml
    
    micromega_plugin.ml
    
    persistent_cache.ml
    
    polynomial.ml
    
    simplex.ml
    
    vect.ml
  - nsatz_core_plugin
    
    ideal.ml
    
    nsatz.ml
    
    nsatz_core_plugin.ml
    
    polynom.ml
    
    utile.ml
  - nsatz_plugin
    
    g_nsatz.ml
    
    nsatz_plugin.ml
  - number_string_notation_plugin
    
    g_number_string.ml
    
    number_string.ml
    
    number_string_notation_plugin.ml
  - ring_plugin
    
    g_ring.ml
    
    ring.ml
    
    ring_ast.ml
    
    ring_plugin.ml
  - rocq-runtime.boot
    
    boot.ml
    
    env.ml
    
    path.ml
    
    usage.ml
    
    util.ml
  - rocq-runtime.checklib
    
    analyze.ml
    
    checkFlags.ml
    
    checkInductive.ml
    
    checkLibrary.ml
    
    check_stat.ml
    
    coq_checklib.ml
    
    coqchk_main.ml
    
    mod_checking.ml
    
    safe_checking.ml
    
    validate.ml
    
    values.ml
  - rocq-runtime.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
    
    memprof_coq.ml
    
    monad.ml
    
    mutex_aux.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
    
    writeOnceArray.ml
  - rocq-runtime.config
    
    coq_config.ml
  - rocq-runtime.coqargs
    
    coqargs.ml
  - rocq-runtime.coqdeplib
    
    args.ml
    
    common.ml
    
    coqdeplib.ml
    
    dep_info.ml
    
    error.ml
    
    file_util.ml
    
    fl.ml
    
    lexer.ml
    
    loadpath.ml
    
    makefile.ml
    
    rocqdep_main.ml
  - rocq-runtime.coqworkmgrapi
    
    coqworkmgrApi.ml
  - rocq-runtime.debugger_support
    
    debugger_support.ml
  - rocq-runtime.dev
    
    top_printers.ml
    
    vm_printers.ml
  - rocq-runtime.engine
    
    eConstr.ml
    
    evar_kinds.ml
    
    evarnames.ml
    
    evarutil.ml
    
    evd.ml
    
    ftactic.ml
    
    logic_monad.ml
    
    namegen.ml
    
    nameops.ml
    
    polyFlags.ml
    
    profile_tactic.ml
    
    proofview.ml
    
    proofview_monad.ml
    
    termops.ml
    
    uState.ml
    
    univFlex.ml
    
    univGen.ml
    
    univMinim.ml
    
    univNames.ml
    
    univProblem.ml
    
    univSubst.ml
  - rocq-runtime.gramlib
    
    gramext.ml
    
    gramlib.ml
    
    grammar.ml
    
    lStream.ml
    
    stream.ml
  - rocq-runtime.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
    
    primNotations.ml
    
    reserve.ml
    
    smartlocate.ml
  - rocq-runtime.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
    
    hConstr.ml
    
    indTyping.ml
    
    indtypes.ml
    
    inductive.ml
    
    inferCumulativity.ml
    
    mod_declarations.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
    
    pConstraints.ml
    
    parray.ml
    
    partial_subst.ml
    
    primred.ml
    
    pstring.ml
    
    qGraph.ml
    
    redFlags.ml
    
    reduction.ml
    
    relevanceops.ml
    
    retroknowledge.ml
    
    rtree.ml
    
    safe_typing.ml
    
    section.ml
    
    sorts.ml
    
    subtyping.ml
    
    term.ml
    
    transparentState.ml
    
    type_errors.ml
    
    typeops.ml
    
    uGraph.ml
    
    uVars.ml
    
    uint63.ml
    
    univ.ml
    
    vars.ml
    
    vconv.ml
    
    vm.ml
    
    vmbytecodes.ml
    
    vmbytegen.ml
    
    vmemitcodes.ml
    
    vmerrors.ml
    
    vmlambda.ml
    
    vmlibrary.ml
    
    vmopcodes.ml
    
    vmsymtable.ml
    
    vmvalues.ml
  - rocq-runtime.lib
    
    acyclicGraph.ml
    
    aux_file.ml
    
    cAst.ml
    
    cDebug.ml
    
    cErrors.ml
    
    cWarnings.ml
    
    control.ml
    
    coqProject_file.ml
    
    dAst.ml
    
    deprecation.ml
    
    envars.ml
    
    feedback.ml
    
    flags.ml
    
    hook.ml
    
    instr.ml
    
    loc.ml
    
    newProfile.ml
    
    objFile.ml
    
    pp.ml
    
    pp_diff.ml
    
    quickfix.ml
    
    spawn.ml
    
    stateid.ml
    
    system.ml
    
    userWarn.ml
    
    util.ml
  - rocq-runtime.library
    
    coqlib.ml
    
    global.ml
    
    globnames.ml
    
    goptions.ml
    
    lib.ml
    
    libnames.ml
    
    libobject.ml
    
    library_info.ml
    
    locality.ml
    
    nametab.ml
    
    rocqlib.ml
    
    summary.ml
  - rocq-runtime.parsing
    
    cLexer.ml
    
    extend.ml
    
    g_constr.ml
    
    g_prim.ml
    
    notgram_ops.ml
    
    pcoq.ml
    
    procq.ml
    
    tok.ml
  - rocq-runtime.perf
    
    perf.ml
  - rocq-runtime.pretyping
    
    arguments_renaming.ml
    
    cases.ml
    
    cbv.ml
    
    coercion.ml
    
    coercionops.ml
    
    combinators.ml
    
    constr_matching.ml
    
    detyping.ml
    
    evaluable.ml
    
    evarconv.ml
    
    evardefine.ml
    
    evarsolve.ml
    
    find_subterm.ml
    
    genarg.ml
    
    geninterp.ml
    
    gensubst.ml
    
    globEnv.ml
    
    glob_ops.ml
    
    heads.ml
    
    inductiveops.ml
    
    keys.ml
    
    libBinding.ml
    
    locusops.ml
    
    nativenorm.ml
    
    patternops.ml
    
    pretype_errors.ml
    
    pretyping.ml
    
    printingFlags.ml
    
    program.ml
    
    reductionops.ml
    
    retyping.ml
    
    structures.ml
    
    tacred.ml
    
    templateArity.ml
    
    typeclasses.ml
    
    typeclasses_errors.ml
    
    typing.ml
    
    unification.ml
    
    vnorm.ml
  - rocq-runtime.printing
    
    genprint.ml
    
    ppconstr.ml
    
    ppextend.ml
    
    pputils.ml
    
    printer.ml
    
    proof_diffs.ml
  - rocq-runtime.proofs
    
    clenv.ml
    
    goal_select.ml
    
    logic.ml
    
    miscprint.ml
    
    proof.ml
    
    proof_bullet.ml
    
    refine.ml
    
    subproof.ml
    
    tacmach.ml
  - rocq-runtime.rocqshim
    
    rocqshim.ml
  - rocq-runtime.stm
    
    asyncTaskQueue.ml
    
    dag.ml
    
    partac.ml
    
    proofBlockDelimiter.ml
    
    spawned.ml
    
    stm.ml
    
    stmargs.ml
    
    tQueue.ml
    
    vcs.ml
    
    workerPool.ml
  - rocq-runtime.sysinit
    
    coqinit.ml
    
    coqloadpath.ml
  - rocq-runtime.tactics
    
    abstract.ml
    
    allScheme.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
    
    fixTactics.ml
    
    generalize.ml
    
    gentactic.ml
    
    hints.ml
    
    hipattern.ml
    
    ind_tables.ml
    
    indrec.ml
    
    induction.ml
    
    inv.ml
    
    ppred.ml
    
    redexpr.ml
    
    redops.ml
    
    rewrite.ml
    
    stdarg.ml
    
    tacticErrors.ml
    
    tacticals.ml
    
    tactics.ml
  - rocq-runtime.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
    
    workerLoop.ml
  - rocq-runtime.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
    
    comRewriteRule.ml
    
    comSearch.ml
    
    comTactic.ml
    
    debugHook.ml
    
    declare.ml
    
    declareInd.ml
    
    declareUniv.ml
    
    declaremods.ml
    
    egramml.ml
    
    egramrocq.ml
    
    future.ml
    
    g_obligations.ml
    
    g_proofs.ml
    
    g_redexpr.ml
    
    g_vernac.ml
    
    himsg.ml
    
    indschemes.ml
    
    library.ml
    
    loadpath.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
    
    tactic_option.ml
    
    topfmt.ml
    
    vernacControl.ml
    
    vernac_classifier.ml
    
    vernacentries.ml
    
    vernacextend.ml
    
    vernacinterp.ml
    
    vernacoptions.ml
    
    vernacprop.ml
    
    vernacstate.ml
    
    vernactypes.ml
  - rocq-runtime.vm
    
    coqrun.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
  - tuto4_plugin
    
    myexternals.ml
    
    tuto4_plugin.ml
  - zify_plugin
    
    g_zify.ml
    
    zify.ml
    
    zify_plugin.ml

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

Module `Indrec`Source

Sourcetype dep_flag = bool

Eliminations

Sourcetype recursion_scheme_error =

| NotMutualInScheme of Names.inductive * Names.inductive
| DuplicateInductiveBlock of Names.inductive

Errors related to recursors building

Sourceexception RecursionSchemeError of Environ.env * recursion_scheme_error

Source

val build_case_analysis_scheme : 
  Environ.env ->
  Evd.evar_map ->
  Names.inductive Evd.puniverses ->
  dep_flag ->
  EConstr.ESorts.t ->
  Evd.evar_map * EConstr.constr * EConstr.constr

Source

val build_induction_scheme : 
  Environ.env ->
  Evd.evar_map ->
  Names.inductive Evd.puniverses ->
  dep_flag ->
  EConstr.ESorts.t ->
  Evd.evar_map * EConstr.constr

Builds a recursive induction scheme (Peano-induction style) in the given sort.

Source

val build_mutual_induction_scheme : 
  Environ.env ->
  Evd.evar_map ->
  ?force_mutual:bool ->
  (Names.inductive * dep_flag * EConstr.ESorts.t) list ->
  Evd.einstance ->
  Evd.evar_map * EConstr.constr list

Builds mutual (recursive) induction schemes

package rocq-runtime

Module IndrecSource

Module `Indrec`Source