package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

coq-lsp
- Library Astdump_plugin
  - Astdump_plugin
    
    Main
- Library Example_plugin
  - Example_plugin
    
    Main
- Library Goaldumpl_plugin
  - Goaldumpl_plugin
    
    Main
- Library Savevo_plugin
  - Savevo_plugin
    
    Main
- Library Unidiff_plugin
  - Unidiff_plugin
    
    Main
- Library coq-lsp.coq
  - Coq
    
    Args
    
    Ast
    
    Id
    
    Set
    
    Map
    
    Require
    
    Meta
    
    Command
    
    Compat
    
    Ocaml_413
    
    String
    
    Ocaml_414
    
    In_channel
    
    Out_channel
    
    Result
    
    O
    
    Option
    
    O
    
    Files
    
    Glob
    
    Info
    
    Goals
    
    Reified_goal
    
    Equality
    
    Init
    
    Interp
    
    Require
    
    Library_file
    
    Entry
    
    Limits
    
    Intf
    
    Token
    
    Coq
    
    Token
    
    Mp
    
    Token
    
    Token
    
    Limits_mp_impl
    
    Token
    
    Loader
    
    Message
    
    Module
    
    Parsing
    
    Parsable
    
    Print
    
    Protect
    
    Error
    
    R
    
    E
    
    O
    
    Save
    
    State
    
    Proof
    
    Declare
    
    OblState
    
    View
    
    Obl
    
    Utils
    
    Workspace
    
    Flags
    
    Warning
    
    Require
    
    CmdLine
- Library coq-lsp.fleche
  - Fleche
    
    Config
    
    Unicode_completion
    
    Contents
    
    R
    
    Debug
    
    Doc
    
    Node
    
    Ast
    
    Info
    
    Message
    
    Completion
    
    Env
    
    Target
    
    Info
    
    Point
    
    LineCol
    
    Offset
    
    S
    
    P
    
    LC
    
    O
    
    Goals
    
    Completion
    
    Io
    
    Level
    
    CallBack
    
    Log
    
    Report
    
    Memo
    
    Stats
    
    Intern
    
    S
    
    Init
    
    Interp
    
    Require
    
    Admit
    
    GlobalCacheStats
    
    Perf
    
    Info
    
    Sentence
    
    Perf_analysis
    
    Progress
    
    Info
    
    ServerInfo
    
    Version
    
    Status
    
    Stats
    
    Kind
    
    Global
    
    Theory
    
    Check
    
    Request
    
    Register
    
    InjectRequire
    
    Completed
    
    Version
- Library coq-lsp.lang
  - Lang
    
    Ast
    
    Name
    
    Info
    
    Compat
    
    OCaml4_14
    
    Uchar
    
    String
    
    Diagnostic
    
    Data
    
    Severity
    
    LUri
    
    File
    
    Point
    
    Range
    
    Utf
    
    Encoding
    
    With_range
- Library coq-lsp.lsp
  - Lsp
    
    Base
    
    Params
    
    Notification
    
    Request
    
    Response
    
    Message
    
    ProgressToken
    
    ProgressParams
    
    WorkDoneProgressBegin
    
    WorkDoneProgressReport
    
    WorkDoneProgressEnd
    
    Core
    
    Location
    
    LocationLink
    
    DocumentSymbol
    
    SymInfo
    
    HoverContents
    
    HoverInfo
    
    LabelDetails
    
    TextEditReplace
    
    CompletionData
    
    Command
    
    CodeLens
    
    SelectionRange
    
    PublishDiagnosticsParams
    
    DocumentDiagnosticParams
    
    FullDocumentDiagnosticReport
    
    UnchangedDocumentDiagnosticReport
    
    DocumentDiagnosticReportPartialResult
    
    Doc
    
    TextDocumentItem
    
    TextDocumentIdentifier
    
    OVersionedTextDocumentIdentifier
    
    VersionedTextDocumentIdentifier
    
    Io
    
    TraceValue
    
    Lvl
    
    MessageParams
    
    TraceParams
    
    JCoq
    
    Loc
    
    Names
    
    Evar
    
    Evar_kinds
    
    Pp
    
    Goals
    
    Reified_goal
    
    Goals_
    
    Ast
    
    Declare
    
    OblState
    
    View
    
    Obl
    
    JFleche
    
    Config
    
    FileProgress
    
    Message
    
    GoalsAnswer
    
    CompletionStatus
    
    RangedSpan
    
    FlecheDocument
    
    SentencePerfData
    
    DocumentPerfData
    
    JLang
    
    Point
    
    Range
    
    LUri
    
    File
    
    Diagnostic
    
    Point
    
    Range
    
    Workspace
    
    WorkspaceFolder
    
    WorkspaceFoldersChangeEvent
    
    DidChangeWorkspaceFoldersParams
- Library coq-lsp.petanque
  - Petanque
    
    Agent
    
    State
    
    Inspect
    
    Proof
    
    Error
    
    R
    
    Run_opts
    
    Run_result
    
    Premise
    
    Info
- Library coq-lsp.serlib
  - Serlib
    
    SerType
    
    SJHC
    
    SJHC1
    
    Bijectable
    
    Biject
    
    Bijectable1
    
    Biject1
    
    Pierceable
    
    Pierceable1
    
    Pierce
    
    Pierce1
    
    OpaqueDesc
    
    Opaque
    
    OpaqueDesc1
    
    Opaque1
    
    Ser_attributes
    
    CAst
    
    Ser_cAst
    
    Ser_cEphemeron
    
    EBiject
    
    B
    
    Ser_cMap
    
    ExtS
    
    Make
    
    Ser_cPrimitives
    
    PTP
    
    Prim_type_
    
    OOTP
    
    Op_or_type_
    
    Ser_cSet
    
    ExtS
    
    Make
    
    Ser_cUnix
    
    Ser_class_tactics
    
    Ser_constr
    
    Ser_constr_matching
    
    Ser_constrexpr
    
    Ser_context
    
    Rel
    
    Declaration
    
    Named
    
    Declaration
    
    Compacted
    
    Declaration
    
    Ser_conv_oracle
    
    Ser_cooking
    
    Ser_coqargs
    
    Names
    
    Ser_dAst
    
    Ser_declarations
    
    Ser_declaremods
    
    Ser_decls
    
    Ser_deprecation
    
    Ser_eConstr
    
    Ser_entries
    
    Stateid
    
    Future
    
    Names
    
    Univ
    
    Constr
    
    Declarations
    
    CPrimitives
    
    Ser_environ
    
    Ser_equality
    
    Ser_evar
    
    Self
    
    Set
    
    Ser_evar_kinds
    
    Ser_evd
    
    Ser_extend
    
    Ser_feedback
    
    Ser_flags
    
    Ser_float64
    
    PierceSpec
    
    Ser_future
    
    Ser_genarg
    
    GenSer0
    
    GS0
    
    GenSer
    
    GS
    
    Ser_genintern
    
    Store
    
    Ser_geninterp
    
    Val
    
    Ser_genredexpr
    
    Ser_glob_term
    
    Ser_globnames
    
    Names
    
    Ser_goal_select
    
    Names
    
    Ser_goptions
    
    Ser_gramlib
    
    Gramext
    
    Ser_hints
    
    Ser_impargs
    
    Ser_int
    
    Ser_inv
    
    Ser_lib
    
    Nametab
    
    Libobject
    
    Summary
    
    Ser_libnames
    
    Ser_libobject
    
    Names
    
    Mod_subst
    
    CString
    
    Pred
    
    Dyn
    
    Reified
    
    Ser_loadpath
    
    Names
    
    Ser_loc
    
    Ser_locality
    
    Ser_locus
    
    Ser_ltac_pretype
    
    Ser_mod_subst
    
    Ser_namegen
    
    Names
    
    Ser_names
    
    Id
    
    Set
    
    Map
    
    Name
    
    DirPath
    
    DPmap
    
    Label
    
    MBId
    
    ModPath
    
    MPmap
    
    KerName
    
    KNmap
    
    Constant
    
    Cset_env
    
    Cmap
    
    Cmap_env
    
    MutInd
    
    Mindmap
    
    Mindmap_env
    
    Indset_env
    
    Projection
    
    Repr
    
    GlobRef
    
    Ser_nametab
    
    Ser_nativevalues
    
    Names
    
    Evar
    
    Sorts
    
    Constr
    
    Univ
    
    NVI
    
    Ser_notation
    
    Ser_notation_gram
    
    Ser_notation_term
    
    Ser_notationextern
    
    Ser_numTok
    
    Unsigned
    
    PierceSpec
    
    UnsignedNat
    
    USNBij
    
    Signed
    
    Ser_opaqueproof
    
    Ser_pattern
    
    Ser_pp
    
    Ser_ppextend
    
    Ser_pretype_errors
    
    Ser_printer
    
    Names
    
    Ser_proof
    
    Ser_proof_bullet
    
    Ser_range
    
    Ser_reduction
    
    Ser_retroknowledge
    
    Ser_rtree
    
    RTreePierce
    
    Ser_sList
    
    SL
    
    Ser_safe_typing
    
    Ser_sorts
    
    Ser_stateid
    
    Ser_stdarg
    
    Ser_stdlib
    
    Lazy
    
    List
    
    Option
    
    Ser_stm
    
    Ser_summary
    
    Ser_tacred
    
    Names
    
    Ser_tactics
    
    Ser_tactypes
    
    CAst
    
    Names
    
    Namegen
    
    EConstr
    
    DO
    
    B
    
    Ser_tok
    
    Ser_type_errors
    
    Ser_typeclasses
    
    Ser_uGraph
    
    Bound
    
    Ser_uState
    
    Ser_uint63
    
    Ser_univ
    
    Level
    
    Universe
    
    Variance
    
    Instance
    
    Constraints
    
    UContext
    
    AbstractContext
    
    ContextSet
    
    Ser_univNames
    
    Names
    
    Ser_universes
    
    Ser_util
    
    Empty
    
    Ser_vernacexpr
    
    Ser_vernacextend
    
    Names
    
    Ser_vmbytecodes
    
    Names
    
    Evar
    
    Ser_vmemitcodes
    
    Ser_vmvalues
    
    Ser_xml_datatype
    
    Serlib_base
    
    Serlib_init
- Library fleche_waterproof
  - Fleche_waterproof
    
    Json
    
    CAst
    
    Ljson
    
    Tjson
- Library petanque_json
  - Petanque_json
    
    Interp
    
    Action
    
    JAgent
    
    State
    
    Inspect
    
    Stdlib
    
    Result
    
    Result
    
    Result_
    
    Error
    
    Run_opts
    
    Run_result
    
    R
    
    Goals
    
    Lang
    
    Range
    
    With_range
    
    Ast
    
    Name
    
    Info
    
    Premise
    
    Info
    
    Obj_map
    
    Obj
    
    S
    
    Make
    
    Protocol
    
    HType
    
    Handler
    
    Params
    
    Response
    
    Request
    
    S
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    Start
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    RunTac
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    Goals
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    Premises
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    StateEqual
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    StateHash
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    StateProofEqual
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    StateProofHash
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
- Library petanque_shell
  - Petanque_shell
    
    Client
    
    Chans
    
    S
    
    Interp_shell
    
    Protocol_shell
    
    SetWorkspace
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    TableOfContents
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    Shell
- Library serlib_cc
  - Serlib_cc
- Library serlib_extraction
  - Serlib_extraction
    
    Ser_g_extraction
- Library serlib_firstorder
  - Serlib_firstorder
    
    Ser_g_ground
    
    Loc
    
    Names
    
    Libnames
    
    Locus
- Library serlib_funind
  - Serlib_funind
    
    Ser_g_indfun
    
    CAst
    
    Names
    
    Sorts
    
    Libnames
    
    Constrexpr
    
    Tactypes
    
    Genintern
    
    EConstr
    
    Tacexpr
    
    A1
    
    WitFI
    
    WitFS
    
    Loc
    
    Vernacexpr
    
    WFFD
    
    WAU
- Library serlib_ltac
  - Serlib_ltac
    
    Ser_profile_ltac
    
    Ser_rewrite
    
    Ser_tacarg
    
    Ser_tacentries
    
    Ser_tacenv
    
    Ser_tacexpr
- Library serlib_ltac2
  - Serlib_ltac2
    
    Ser_g_ltac2
    
    Tac2expr
    
    L2Entry
    
    L2Expr
    
    Ser_tac2env
    
    Util
    
    Loc
    
    CAst
    
    Names
    
    Tac2expr
    
    WL2
    
    WLC2
    
    WLQ2
    
    WLV2
    
    Ser_tac2expr
    
    Loc
    
    CAst
    
    Names
    
    Libnames
    
    ObjS
    
    Obj
    
    T2ESpec
    
    T2E
    
    GT2ESpec
    
    GT2E
    
    Ser_tac2quote
- Library serlib_micromega
  - Serlib_micromega
- Library serlib_number_string_notation_plugin
  - Serlib_number_string_notation_plugin
    
    Ser_g_number_syntax
    
    Libnames
    
    Notation
    
    A1
    
    A2
    
    A3
    
    A4
    
    A5
    
    A6
    
    Ser_number
    
    Libnames
    
    Notation
- Library serlib_ring
  - Serlib_ring
    
    Ser_g_ring
    
    CAst
    
    Libnames
    
    Constrexpr
    
    Tactypes
    
    Genintern
    
    EConstr
    
    Tacexpr
    
    Ltac_plugin
    
    Tacexpr
    
    A0
    
    A1
    
    A2
    
    A3
- Library serlib_ssr
  - Serlib_ssr
    
    Ser_ssrast
    
    Loc
    
    Names
    
    Locus
    
    Constrexpr
    
    Genintern
    
    Geninterp
    
    Ssrmatching_plugin
    
    Ssrmatching
    
    Ltac_plugin
    
    Tacexpr
    
    Proofview
    
    Ser_ssrequality
    
    Ssrmatching_plugin
    
    Ssrmatching
    
    Ssreflect_plugin
    
    Ssrast
    
    Ssrequality
    
    Ser_ssrparser
    
    Ssrmatching
    
    Ltac_plugin
    
    Tacexpr
    
    Ssrast
    
    Ssreflect_plugin
    
    Ssrast
    
    Ssrequality
    
    Ssrparser
    
    A0
    
    A1
    
    A2
    
    A3
    
    A4
    
    A5
    
    A6
    
    A7
    
    A8
    
    A9
    
    A10
    
    A11
    
    A12
    
    A13
    
    A14
    
    Wrap_ssrast
    
    Ssreflect_plugin
    
    Ssrast
    
    Wrap
- Library serlib_ssrmatching
  - Serlib_ssrmatching
    
    Ser_ssrmatching
    
    Genintern
    
    Geninterp
    
    PierceRPattern
    
    B_
- Library serlib_tauto
  - Serlib_tauto
- Library serlib_zify
  - Serlib_zify
- Sources
  - Astdump_plugin
    
    astdump_plugin.ml
    
    main.ml
  - Example_plugin
    
    example_plugin.ml
    
    main.ml
  - Goaldumpl_plugin
    
    goaldumpl_plugin.ml
    
    main.ml
  - Savevo_plugin
    
    main.ml
    
    savevo_plugin.ml
  - Unidiff_plugin
    
    main.ml
    
    unidiff_plugin.ml
  - coq-lsp.coq
    
    args.ml
    
    ast.ml
    
    compat.ml
    
    coq.ml
    
    files.ml
    
    glob.ml
    
    goals.ml
    
    init.ml
    
    interp.ml
    
    library_file.ml
    
    limits.ml
    
    limits_mp_impl.ml
    
    loader.ml
    
    message.ml
    
    module.ml
    
    parsing.ml
    
    print.ml
    
    protect.ml
    
    save.ml
    
    state.ml
    
    utils.ml
    
    workspace.ml
  - coq-lsp.fleche
    
    config.ml
    
    contents.ml
    
    debug.ml
    
    doc.ml
    
    fleche.ml
    
    info.ml
    
    io.ml
    
    memo.ml
    
    perf.ml
    
    perf_analysis.ml
    
    progress.ml
    
    serverInfo.ml
    
    stats.ml
    
    theory.ml
    
    version.ml
  - coq-lsp.lang
    
    ast.ml
    
    compat.ml
    
    diagnostic.ml
    
    lUri.ml
    
    lang.ml
    
    point.ml
    
    range.ml
    
    utf.ml
    
    with_range.ml
  - coq-lsp.lsp
    
    base.ml
    
    core.ml
    
    doc.ml
    
    io.ml
    
    jCoq.ml
    
    jFleche.ml
    
    jLang.ml
    
    lsp.ml
    
    workspace.ml
  - coq-lsp.petanque
    
    agent.ml
    
    petanque.ml
  - coq-lsp.serlib
    
    serType.ml
    
    ser_attributes.ml
    
    ser_cAst.ml
    
    ser_cEphemeron.ml
    
    ser_cMap.ml
    
    ser_cPrimitives.ml
    
    ser_cSet.ml
    
    ser_cUnix.ml
    
    ser_class_tactics.ml
    
    ser_constr.ml
    
    ser_constr_matching.ml
    
    ser_constrexpr.ml
    
    ser_context.ml
    
    ser_conv_oracle.ml
    
    ser_cooking.ml
    
    ser_coqargs.ml
    
    ser_dAst.ml
    
    ser_declarations.ml
    
    ser_declaremods.ml
    
    ser_decls.ml
    
    ser_deprecation.ml
    
    ser_eConstr.ml
    
    ser_entries.ml
    
    ser_environ.ml
    
    ser_equality.ml
    
    ser_evar.ml
    
    ser_evar_kinds.ml
    
    ser_evd.ml
    
    ser_extend.ml
    
    ser_feedback.ml
    
    ser_flags.ml
    
    ser_float64.ml
    
    ser_future.ml
    
    ser_genarg.ml
    
    ser_genintern.ml
    
    ser_geninterp.ml
    
    ser_genredexpr.ml
    
    ser_glob_term.ml
    
    ser_globnames.ml
    
    ser_goal_select.ml
    
    ser_goptions.ml
    
    ser_gramlib.ml
    
    ser_hints.ml
    
    ser_impargs.ml
    
    ser_int.ml
    
    ser_inv.ml
    
    ser_lib.ml
    
    ser_libnames.ml
    
    ser_libobject.ml
    
    ser_loadpath.ml
    
    ser_loc.ml
    
    ser_locality.ml
    
    ser_locus.ml
    
    ser_ltac_pretype.ml
    
    ser_mod_subst.ml
    
    ser_namegen.ml
    
    ser_names.ml
    
    ser_nametab.ml
    
    ser_nativevalues.ml
    
    ser_notation.ml
    
    ser_notation_gram.ml
    
    ser_notation_term.ml
    
    ser_notationextern.ml
    
    ser_numTok.ml
    
    ser_opaqueproof.ml
    
    ser_pattern.ml
    
    ser_pp.ml
    
    ser_ppextend.ml
    
    ser_pretype_errors.ml
    
    ser_printer.ml
    
    ser_proof.ml
    
    ser_proof_bullet.ml
    
    ser_range.ml
    
    ser_reduction.ml
    
    ser_retroknowledge.ml
    
    ser_rtree.ml
    
    ser_sList.ml
    
    ser_safe_typing.ml
    
    ser_sorts.ml
    
    ser_stateid.ml
    
    ser_stdarg.ml
    
    ser_stdlib.ml
    
    ser_stm.ml
    
    ser_summary.ml
    
    ser_tacred.ml
    
    ser_tactics.ml
    
    ser_tactypes.ml
    
    ser_tok.ml
    
    ser_type_errors.ml
    
    ser_typeclasses.ml
    
    ser_uGraph.ml
    
    ser_uState.ml
    
    ser_uint63.ml
    
    ser_univ.ml
    
    ser_univNames.ml
    
    ser_universes.ml
    
    ser_util.ml
    
    ser_vernacexpr.ml
    
    ser_vernacextend.ml
    
    ser_vmbytecodes.ml
    
    ser_vmemitcodes.ml
    
    ser_vmvalues.ml
    
    ser_xml_datatype.ml
    
    serlib.ml
    
    serlib_base.ml
    
    serlib_init.ml
  - fleche_waterproof
    
    fleche_waterproof.ml
    
    json.ml
    
    ljson.ml
    
    tjson.ml
  - petanque_json
    
    interp.ml
    
    jAgent.ml
    
    obj_map.ml
    
    petanque_json.ml
    
    protocol.ml
  - petanque_shell
    
    client.ml
    
    interp_shell.ml
    
    petanque_shell.ml
    
    protocol_shell.ml
    
    shell.ml
  - serlib_cc
    
    serlib_cc.ml
  - serlib_extraction
    
    ser_g_extraction.ml
    
    serlib_extraction.ml
  - serlib_firstorder
    
    ser_g_ground.ml
    
    serlib_firstorder.ml
  - serlib_funind
    
    ser_g_indfun.ml
    
    serlib_funind.ml
  - serlib_ltac
    
    ser_profile_ltac.ml
    
    ser_rewrite.ml
    
    ser_tacarg.ml
    
    ser_tacentries.ml
    
    ser_tacenv.ml
    
    ser_tacexpr.ml
    
    serlib_ltac.ml
  - serlib_ltac2
    
    ser_g_ltac2.ml
    
    ser_tac2env.ml
    
    ser_tac2expr.ml
    
    ser_tac2quote.ml
    
    serlib_ltac2.ml
  - serlib_micromega
    
    serlib_micromega.ml
  - serlib_number_string_notation_plugin
    
    ser_g_number_syntax.ml
    
    ser_number.ml
    
    serlib_number_string_notation_plugin.ml
  - serlib_ring
    
    ser_g_ring.ml
    
    serlib_ring.ml
  - serlib_ssr
    
    ser_ssrast.ml
    
    ser_ssrequality.ml
    
    ser_ssrparser.ml
    
    serlib_ssr.ml
    
    wrap_ssrast.ml
  - serlib_ssrmatching
    
    ser_ssrmatching.ml
    
    serlib_ssrmatching.ml
  - serlib_tauto
    
    serlib_tauto.ml
  - serlib_zify
    
    serlib_zify.ml

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

Module `Petanque_shell.Interp_shell`Source

type doc_handler =
  token:Coq.Limits.Token.t ->
  uri:Lang.LUri.File.t ->
  (Fleche.Doc.t, Petanque.Agent.Error.t) Result.t

Source

val interp : 
  fn:doc_handler ->
  token:Coq.Limits.Token.t ->
  Lsp.Base.Message.t ->
  Lsp.Base.Message.t option

package coq-lsp

Module Petanque_shell.Interp_shellSource

Module `Petanque_shell.Interp_shell`Source