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_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
  - 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
    
    Severity
  - LUri
    
    File
  - Point
  - 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
    
    Lang
    
    Ast
    
    Info
    
    Name
    
    Range
    
    With_range
    
    Premise
    
    Info
    
    R
    
    Run_opts
    
    Run_result
    
    State
    
    Stdlib
    
    Result
  - 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.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
    
    M
    
    S
  - Ser_cPrimitives
    
    OOTP
    
    Op_or_type_
    
    PTP
    
    Prim_type_
  - Ser_cSet
    
    ExtS
    
    Make
    
    M
    
    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_coqargs
  - Ser_dAst
  - Ser_declarations
  - Ser_declaremods
  - Ser_decls
  - Ser_deprecation
  - Ser_eConstr
  - Ser_entries
  - 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
    
    GS
    
    M
    
    GS0
    
    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_proof_bullet
  - 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_stm
  - Ser_summary
    
    Interp
  - Ser_tacred
  - 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_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.micromega
- Serlib_micromega
coq-lsp.serlib.number_string_notation
- Serlib_number_string_notation_plugin
  - Ser_g_number_syntax
    
    A2
    
    A3
    
    A4
    
    A5
    
    A6
  - Ser_number
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 Error : sig ... end

This modules reifies Coq side effects into an algebraic structure.

module R : sig ... end

This "monad" could be related to "Runners in action" (Ahman, Bauer), thanks to Guillaume Munch-Maccagnoni for the reference and for many useful tips!

module E : sig ... end

val fb_queue : Loc.t Message.t list ref

Must be hooked to allow Protect to capture the feedback.

val eval : token:Limits.Token.t -> f:('i -> 'o) -> 'i -> ('o, Loc.t) E.t

Eval a function and reify the exceptions. Note f _must_ be pure, as in case of anomaly f may be re-executed with debug options. Beware, not thread-safe! token Does allow to interrupt the evaluation.