package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

package coq-lsp

coq-lsp
- Library Example_plugin
  - Example_plugin
    
    Main
- Library coq-lsp.coq
  - Coq
    
    Ast
    
    Id
    
    Set
    
    Map
    
    Goals
    
    Init
    
    Interp
    
    Loader
    
    Message
    
    Parsing
    
    Parsable
    
    Print
    
    Protect
    
    Error
    
    R
    
    E
    
    Save
    
    State
    
    Proof
    
    Utf8
    
    Utils
    
    Workspace
    
    Flags
    
    Warning
    
    CmdLine
- Library coq-lsp.fleche
  - Fleche
    
    Config
    
    Unicode_completion
    
    Contents
    
    R
    
    Debug
    
    Doc
    
    Node
    
    Ast
    
    Info
    
    Message
    
    Completion
    
    Target
    
    Info
    
    Point
    
    LineCol
    
    Offset
    
    S
    
    P
    
    LC
    
    O
    
    Goals
    
    Completion
    
    Io
    
    CallBack
    
    Log
    
    Report
    
    Memo
    
    Stats
    
    Init
    
    Interp
    
    Admit
    
    CacheStats
    
    Perf
    
    Sentence
    
    Perf_analysis
    
    Progress
    
    Info
    
    Stats
    
    Kind
    
    Theory
    
    Check
    
    Request
    
    Register
    
    Completed
    
    Version
- Library coq-lsp.lang
  - Lang
    
    Ast
    
    Name
    
    Info
    
    Diagnostic
    
    Extra
    
    LUri
    
    File
    
    Point
    
    Range
    
    With_range
- Library coq-lsp.lsp
  - Lsp
    
    Base
    
    Message
    
    ProgressToken
    
    ProgressParams
    
    WorkDoneProgressBegin
    
    WorkDoneProgressReport
    
    WorkDoneProgressEnd
    
    Core
    
    Location
    
    LocationLink
    
    DocumentSymbol
    
    SymInfo
    
    HoverContents
    
    HoverInfo
    
    LabelDetails
    
    TextEditReplace
    
    CompletionData
    
    Command
    
    CodeLens
    
    SelectionRange
    
    DocumentDiagnosticParams
    
    FullDocumentDiagnosticReport
    
    UnchangedDocumentDiagnosticReport
    
    DocumentDiagnosticReportPartialResult
    
    Doc
    
    TextDocumentItem
    
    TextDocumentIdentifier
    
    OVersionedTextDocumentIdentifier
    
    VersionedTextDocumentIdentifier
    
    Io
    
    TraceValue
    
    JCoq
    
    Loc
    
    Names
    
    Evar
    
    Evar_kinds
    
    Pp
    
    Goals
    
    Goals_
    
    Ast
    
    Declare
    
    OblState
    
    View
    
    Obl
    
    JFleche
    
    Config
    
    FileProgress
    
    Message
    
    GoalsAnswer
    
    CompletionStatus
    
    RangedSpan
    
    FlecheDocument
    
    SentencePerfData
    
    DocumentPerfData
    
    JLang
    
    Point
    
    Range
    
    LUri
    
    File
    
    Diagnostic
    
    Workspace
    
    WorkspaceFolder
    
    WorkspaceFoldersChangeEvent
    
    DidChangeWorkspaceFoldersParams
- Library fleche_waterproof
  - Fleche_waterproof
    
    Json
    
    CAst
    
    Ljson
    
    Tjson
- Sources
  - Example_plugin
    
    example_plugin.ml
    
    main.ml
  - coq-lsp.coq
    
    ast.ml
    
    coq.ml
    
    goals.ml
    
    init.ml
    
    interp.ml
    
    loader.ml
    
    message.ml
    
    parsing.ml
    
    print.ml
    
    protect.ml
    
    save.ml
    
    state.ml
    
    utf8.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
    
    stats.ml
    
    theory.ml
    
    version.ml
  - coq-lsp.lang
    
    ast.ml
    
    diagnostic.ml
    
    lUri.ml
    
    lang.ml
    
    point.ml
    
    range.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
  - fleche_waterproof
    
    fleche_waterproof.ml
    
    json.ml
    
    ljson.ml
    
    tjson.ml

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

Module `Memo.Interp`Source

Sourcetype t = Coq.State.t * Coq.Ast.t

Sourceval eval : t -> Coq.State.t Coq.Interp.interp_result Stats.t

Interpret a command, possibly memoizing it

Sourceval size : unit -> int

size () Return the size in words, expensive

Sourceval input_info : t -> string

debug

package coq-lsp

Module Memo.InterpSource

Module `Memo.Interp`Source