package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

package coq-lsp

coq-lsp.coq
- Coq
  - Args
  - Ast
    
    Id
    
    Meta
    
    Command
    
    Require
  - Compat
    
    Ocaml_413
    
    String
    
    Ocaml_414
    
    In_channel
    
    Out_channel
    
    Option
    
    O
    
    Result
    
    O
  - Files
  - Glob
    
    Info
  - Goals
    
    Equality
    
    Reified_goal
  - Init
  - Interp
    
    Require
  - Library_file
    
    Entry
  - Limits
    
    Coq
    
    Token
    
    Intf
    
    Token
    
    Mp
    
    Token
    
    Token
  - Limits_mp_impl
    
    Token
  - Loader
  - Message
    
    Payload
  - Module
  - Parsing
    
    Parsable
  - Print
  - Protect
    
    E
    
    O
    
    Error
    
    R
  - Save
  - State
    
    Proof
  - Utils
  - Workspace
    
    CmdLine
    
    Flags
    
    Require
    
    Warning
coq-lsp.fleche
- Fleche
  - Config
    
    Unicode_completion
  - Contents
    
    R
  - Debug
  - Doc
    
    Completion
    
    Env
    
    Node
    
    Ast
    
    Info
    
    Message
    
    Target
  - Info
    
    Completion
    
    Goals
    
    LC
    
    LineCol
    
    O
    
    Offset
    
    Point
    
    S
    
    P
  - Io
    
    CallBack
    
    Level
    
    Log
    
    Report
  - Memo
    
    Admit
    
    GlobalCacheStats
    
    Init
    
    Intern
    
    Interp
    
    Require
    
    S
    
    Stats
  - Perf
    
    Info
    
    Sentence
  - Perf_analysis
  - Progress
    
    Info
  - ServerInfo
    
    Status
    
    Version
  - Stats
    
    Global
    
    Kind
  - Theory
    
    Check
    
    Register
    
    Completed
    
    InjectRequire
    
    Request
  - Version
coq-lsp.fleche.waterproof
- Fleche_waterproof
  - Json
    
    CAst
  - Ljson
  - Tjson
coq-lsp.lang
- Lang
  - Ast
    
    Info
    
    Name
  - Compat
    
    OCaml4_14
    
    String
    
    Uchar
  - Diagnostic
    
    Data
    
    FailedRequire
    
    Severity
  - LUri
    
    File
  - Point
  - Qf
  - Range
  - Utf
    
    Encoding
  - With_range
coq-lsp.lsp
- Lsp
coq-lsp.petanque
- Petanque
  - Agent
    
    Error
    
    Premise
    
    Info
    
    R
    
    Run_opts
    
    Run_result
    
    State
    
    Inspect
    
    Proof
coq-lsp.petanque.json
- Petanque_json
  - Interp
    
    Action
  - JAgent
    
    Error
    
    Goals
    
    Inspect
    
    Premise
    
    Info
    
    R
    
    Run_opts
    
    Run_result
    
    State
  - Obj_map
    
    Make
    
    O
    
    Obj
    
    S
  - Protocol
    
    Goals
    
    Handler
    
    Params
    
    Params
    
    Response
    
    HType
    
    Handler
    
    Params
    
    Response
    
    Premises
    
    Handler
    
    Params
    
    Params
    
    Response
    
    Request
    
    S
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    RunTac
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    Start
    
    Handler
    
    Response
    
    Params
    
    Response
    
    StateEqual
    
    Handler
    
    Params
    
    Params
    
    Response
    
    StateHash
    
    Handler
    
    Params
    
    Params
    
    Response
    
    StateProofEqual
    
    Handler
    
    StateProofHash
    
    Handler
    
    Response
coq-lsp.petanque.json_shell
- Petanque_shell
  - Client
    
    Chans
    
    S
    
    C
  - Interp_shell
  - Protocol_shell
    
    SetWorkspace
    
    Handler
    
    Params
    
    Response
    
    TableOfContents
    
    Handler
    
    Params
    
    Response
  - Shell
coq-lsp.plugin.astdump
- Astdump_plugin
  - Main
coq-lsp.plugin.example
- Example_plugin
  - Main
coq-lsp.plugin.explain_errors
- Explain_errors
  - Main
coq-lsp.plugin.goaldump
- Goaldumpl_plugin
  - Main
coq-lsp.plugin.save_vo
- Savevo_plugin
  - Main
coq-lsp.plugin.univdiff
- Unidiff_plugin
  - Main
coq-lsp.serlib
- Serlib
  - SerType
    
    Biject
    
    M
    
    Biject1
    
    M
    
    Bijectable
    
    Bijectable1
    
    Opaque
    
    M
    
    Opaque1
    
    M
    
    OpaqueDesc
    
    OpaqueDesc1
    
    Pierce
    
    M
    
    Pierce1
    
    M
    
    Pierceable
    
    Pierceable1
    
    SJHC
    
    SJHC1
  - Ser_attributes
  - Ser_cAst
  - Ser_cEphemeron
    
    B
    
    EBiject
  - Ser_cMap
    
    ExtS
    
    Make
    
    S
  - Ser_cPrimitives
    
    OOTP
    
    Op_or_type_
    
    PTP
    
    Prim_type_
  - Ser_cSet
    
    ExtS
    
    Make
    
    S
  - Ser_cUnix
  - Ser_class_tactics
  - Ser_constr
  - Ser_constr_matching
  - Ser_constrexpr
  - Ser_context
    
    Compacted
    
    Declaration
    
    Named
    
    Declaration
    
    Rel
    
    Declaration
  - Ser_conv_oracle
  - Ser_cooking
  - Ser_dAst
  - Ser_declarations
  - Ser_declaremods
  - Ser_decls
  - Ser_deprecation
  - Ser_eConstr
    
    ERelevance
  - Ser_entries
  - Ser_environ
  - Ser_equality
  - Ser_evaluable
  - Ser_evar
    
    Self
    
    Set
  - Ser_evar_kinds
  - Ser_evd
  - Ser_extend
  - Ser_feedback
  - Ser_flags
  - Ser_float64
    
    PierceSpec
  - Ser_future
  - Ser_genarg
    
    GS
    
    M
    
    GS0
    
    M
    
    GSV
    
    M
    
    GenSer
    
    GenSer0
  - Ser_genintern
    
    Store
  - Ser_geninterp
    
    Val
  - Ser_genredexpr
  - Ser_glob_term
  - Ser_globnames
  - Ser_goal_select
  - Ser_goptions
  - Ser_gramlib
    
    Gramext
  - Ser_hints
  - Ser_impargs
  - Ser_int
  - Ser_inv
  - Ser_lib
  - Ser_libnames
  - Ser_libobject
    
    CString
    
    Pred
    
    Dyn
    
    Reified
  - Ser_loadpath
  - Ser_loc
  - Ser_locality
  - Ser_locus
  - Ser_ltac_pretype
  - Ser_mod_subst
  - Ser_namegen
  - Ser_names
    
    Cmap
    
    Cmap_env
    
    Constant
    
    Cset_env
    
    DPmap
    
    DirPath
    
    GlobRef
    
    Id
    
    Map
    
    Set
    
    Indmap_env
    
    Indset_env
    
    KNmap
    
    KerName
    
    Label
    
    MBId
    
    MPmap
    
    Mindmap
    
    Mindmap_env
    
    ModPath
    
    MutInd
    
    Name
    
    Projection
    
    Repr
  - Ser_nametab
  - Ser_nativevalues
    
    NVI
  - Ser_notation
  - Ser_notation_gram
  - Ser_notation_term
  - Ser_notationextern
  - Ser_numTok
    
    Signed
    
    Unsigned
    
    PierceSpec
    
    UnsignedNat
    
    USNBij
  - Ser_opaqueproof
  - Ser_pattern
  - Ser_pp
  - Ser_ppextend
  - Ser_pretype_errors
  - Ser_printer
  - Ser_profile_tactic
  - Ser_proof_bullet
  - Ser_pstring
    
    StrSpec
  - Ser_range
  - Ser_reduction
  - Ser_retroknowledge
  - Ser_rtree
    
    RTreePierce
  - Ser_sList
    
    SL
  - Ser_safe_typing
  - Ser_sorts
    
    QConstraints
    
    QVar
    
    Set
    
    Quality
    
    Set
  - Ser_stateid
  - Ser_stdarg
  - Ser_stdlib
    
    Lazy
    
    List
  - Ser_summary
    
    Interp
  - Ser_tactics
  - Ser_tactypes
    
    B
    
    DO
  - Ser_tok
  - Ser_type_errors
  - Ser_typeclasses
  - Ser_uGraph
    
    Bound
  - Ser_uState
  - Ser_uint63
  - Ser_univ
    
    Constraints
    
    ContextSet
    
    Level
    
    Universe
  - Ser_univNames
  - Ser_universes
  - Ser_util
    
    Empty
  - Ser_uvars
    
    AbstractContext
    
    Instance
    
    UContext
    
    Variance
  - Ser_vernacexpr
  - Ser_vernacextend
  - Ser_vmbytecodes
  - Ser_vmemitcodes
  - Ser_vmlibrary
  - Ser_vmvalues
  - Ser_xml_datatype
  - Serlib_base
  - Serlib_init
coq-lsp.serlib.btauto
- Serlib_btauto
coq-lsp.serlib.cc
- Serlib_cc
coq-lsp.serlib.extraction
- Serlib_extraction
  - Ser_g_extraction
    
    Extraction_plugin
    
    Table
    
    WitII
    
    WitL
    
    WitMN
coq-lsp.serlib.firstorder
- Serlib_firstorder
  - Ser_g_ground
coq-lsp.serlib.funind
- Serlib_funind
  - Ser_g_indfun
    
    A1
    
    WAU
    
    WFFD
    
    WitFI
    
    WitFS
coq-lsp.serlib.ltac
- Serlib_ltac
coq-lsp.serlib.ltac2
- Serlib_ltac2
  - Ser_g_ltac2
    
    L2Entry
    
    L2Expr
  - Ser_tac2env
    
    WL2in1
    
    WL2in1V
    
    WLC2
    
    WLQ2
    
    WLV2
  - Ser_tac2expr
    
    GT2E
    
    GT2ESpec
    
    Obj
    
    ObjS
    
    T2E
    
    T2ESpec
  - Ser_tac2quote
coq-lsp.serlib.ltac2_ltac1
- Serlib_ltac2_ltac1
  - Ser_tac2quote_ltac1
coq-lsp.serlib.micromega
- Serlib_micromega
coq-lsp.serlib.micromega_core
- Serlib_micromega_core
coq-lsp.serlib.number_string_notation
- Serlib_number_string_notation_plugin
  - Ser_g_number_syntax
    
    A2
    
    A3
    
    A4
    
    A5
    
    A6
  - Ser_number_string
coq-lsp.serlib.ring
- Serlib_ring
  - Ser_g_ring
    
    A0
    
    A1
    
    A2
    
    A3
    
    Ltac_plugin
coq-lsp.serlib.ssreflect
- Serlib_ssr
  - Ser_ssrast
    
    Ltac_plugin
    
    Proofview
    
    Ssrmatching_plugin
  - Ser_ssrequality
    
    Ssreflect_plugin
    
    Ssrmatching_plugin
  - Ser_ssrparser
    
    A0
    
    A1
    
    A10
    
    A11
    
    A12
    
    A13
    
    A14
    
    A2
    
    A3
    
    A4
    
    A5
    
    A6
    
    A7
    
    A8
    
    A9
    
    Ltac_plugin
    
    Ssreflect_plugin
  - Wrap_ssrast
    
    Ssreflect_plugin
    
    Wrap
coq-lsp.serlib.ssrmatching
- Serlib_ssrmatching
  - Ser_ssrmatching
coq-lsp.serlib.tauto
- Serlib_tauto
coq-lsp.serlib.zify
- Serlib_zify

Legend:
Library
Module
Module type
Parameter
Class
Class type

module SerType : sig ... end

module Ser_attributes : sig ... end

module Ser_cAst : sig ... end

module Ser_cEphemeron : sig ... end

module Ser_cMap : sig ... end

module Ser_cPrimitives : sig ... end

module Ser_cSet : sig ... end

module Ser_cUnix : sig ... end

module Ser_class_tactics : sig ... end

module Ser_constr : sig ... end

module Ser_constr_matching : sig ... end

module Ser_constrexpr : sig ... end

module Ser_context : sig ... end

module Ser_conv_oracle : sig ... end

module Ser_cooking : sig ... end

module Ser_dAst : sig ... end

module Ser_declarations : sig ... end

module Ser_declaremods : sig ... end

module Ser_decls : sig ... end

module Ser_deprecation : sig ... end

module Ser_eConstr : sig ... end

module Ser_entries : sig ... end

module Ser_environ : sig ... end

module Ser_equality : sig ... end

module Ser_evaluable : sig ... end

module Ser_evar : sig ... end

module Ser_evar_kinds : sig ... end

module Ser_evd : sig ... end

module Ser_extend : sig ... end

module Ser_feedback : sig ... end

module Ser_flags : sig ... end

module Ser_float64 : sig ... end

module Ser_future : sig ... end

module Ser_genarg : sig ... end

module Ser_genintern : sig ... end

module Ser_geninterp : sig ... end

module Ser_genredexpr : sig ... end

module Ser_glob_term : sig ... end

module Ser_globnames : sig ... end

module Ser_goal_select : sig ... end

module Ser_goptions : sig ... end

module Ser_gramlib : sig ... end

module Ser_hints : sig ... end

module Ser_impargs : sig ... end

module Ser_int : sig ... end

module Ser_inv : sig ... end

module Ser_lib : sig ... end

module Ser_libnames : sig ... end

module Ser_libobject : sig ... end

module Ser_loadpath : sig ... end

module Ser_loc : sig ... end

module Ser_locality : sig ... end

module Ser_locus : sig ... end

module Ser_ltac_pretype : sig ... end

module Ser_mod_subst : sig ... end

module Ser_namegen : sig ... end

module Ser_names : sig ... end

module Ser_nametab : sig ... end

module Ser_nativevalues : sig ... end

module Ser_notation : sig ... end

module Ser_notation_gram : sig ... end

module Ser_notation_term : sig ... end

module Ser_notationextern : sig ... end

module Ser_numTok : sig ... end

module Ser_opaqueproof : sig ... end

module Ser_pattern : sig ... end

module Ser_pp : sig ... end

module Ser_ppextend : sig ... end

module Ser_pretype_errors : sig ... end

module Ser_printer : sig ... end

module Ser_profile_tactic : sig ... end

module Ser_proof_bullet : sig ... end

module Ser_pstring : sig ... end

module Ser_range : sig ... end

module Ser_reduction : sig ... end

module Ser_retroknowledge : sig ... end

module Ser_rtree : sig ... end

module Ser_sList : sig ... end

module Ser_safe_typing : sig ... end

module Ser_sorts : sig ... end

module Ser_stateid : sig ... end

module Ser_stdarg : sig ... end

module Ser_stdlib : sig ... end

module Ser_summary : sig ... end

module Ser_tactics : sig ... end

module Ser_tactypes : sig ... end

module Ser_tok : sig ... end

module Ser_type_errors : sig ... end

module Ser_typeclasses : sig ... end

module Ser_uGraph : sig ... end

module Ser_uState : sig ... end

module Ser_uint63 : sig ... end

module Ser_univ : sig ... end

module Ser_univNames : sig ... end

module Ser_universes : sig ... end

module Ser_util : sig ... end

module Ser_uvars : sig ... end

module Ser_vernacexpr : sig ... end

module Ser_vernacextend : sig ... end

module Ser_vmbytecodes : sig ... end

module Ser_vmemitcodes : sig ... end

module Ser_vmlibrary : sig ... end

module Ser_vmvalues : sig ... end

module Ser_xml_datatype : sig ... end

module Serlib_base : sig ... end

module Serlib_init : sig ... end