package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

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

Legend:
Library
Module
Module type
Parameter
Class
Class type

Only used as EConstr internals

type handle

val empty_handle : handle

val liftn_handle : int -> handle -> handle

val kind : 
  evar_map ->
  handle ->
  econstr ->
  handle
  * (econstr,
      econstr,
      MiniEConstr.ESorts.t,
      MiniEConstr.EInstance.t,
      MiniEConstr.ERelevance.t)
      Constr.kind_of_term

val expand : evar_map -> handle -> econstr -> econstr

val expand_instance : 
  skip:bool ->
  undefined evar_info ->
  handle ->
  econstr SList.t ->
  econstr SList.t