package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

coq-lsp.coq
- Coq
  - Args
  - Ast
    
    Id
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Set
    
    Meta
    
    Command
    
    Require
  - Compat
    
    Ocaml_414
    
    In_channel
    
    Out_channel
    
    Result
    
    O
  - Files
  - Glob
    
    Info
  - Goals
  - Init
  - Interp
    
    Require
  - Library_file
    
    Entry
  - Limits
    
    Coq
    
    Token
    
    Intf
    
    Token
    
    Mp
    
    Token
    
    Token
  - Limits_mp_impl
    
    Token
  - Loader
  - Message
  - 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
    
    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
  - Diagnostic
    
    Data
    
    Severity
  - LUri
    
    File
  - Point
  - Range
  - Utf
    
    Encoding
  - With_range
coq-lsp.lsp
- Lsp
coq-lsp.petanque
- Petanque
  - Agent
    
    Env
    
    Error
    
    Premise
    
    R
    
    Run_result
    
    State
coq-lsp.petanque.json
- Petanque_json
  - Client
    
    Chans
    
    S
    
    C
  - Interp
  - JAgent
    
    Env
    
    Error
    
    Goals
    
    Lang
    
    Range
    
    Premise
    
    R
    
    Run_result
    
    State
    
    Stdlib
    
    Result
  - Obj_map
    
    Make
    
    O
    
    Obj
    
    S
  - Protocol
    
    Goals
    
    Handler
    
    Params
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    Init
    
    Handler
    
    Response
    
    Params
    
    Response
    
    Message
    
    Params
    
    Notification
    
    S
    
    Params
    
    Premises
    
    Handler
    
    Params
    
    Params
    
    Response
    
    Request
    
    S
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    RunTac
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    Start
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    Trace
    
    Params
  - Utils
coq-lsp.plugin.astdump
- Astdump_plugin
  - Main
coq-lsp.plugin.example
- Example_plugin
  - Main
coq-lsp.plugin.goaldump
- Goaldumpl_plugin
  - Main
coq-lsp.plugin.save_vo
- Savevo_plugin
  - Main

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Stats : sig ... end

module type S = sig ... end

Flèche memo / cache tables, with some advanced features

module Init : 
  S
    with type input = Coq.State.t * Coq.Workspace.t * Lang.LUri.File.t
     and type output = Coq.State.t

Document creation cache

module Interp : 
  S with type input = Coq.State.t * Coq.Ast.t and type output = Coq.State.t

Vernacular evaluation cache, invariant w.r.t. Coq's Ast locations, results are repaired.

module Require : 
  S
    with type input = Coq.State.t * Coq.Files.t * Coq.Ast.Require.t
     and type output = Coq.State.t

Require evaluation cache, also invariant w.r.t. locations inside Coq.Ast.Require.t

module Admit : S with type input = Coq.State.t and type output = Coq.State.t

Admit evaluation cache

module GlobalCacheStats : sig ... end

val all_size : unit -> int

Size of all caches, very expensive