package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

Language Server Protocol native server for Coq

Install

sha256=bd1d61581eed552aef1b2a37442684a9f96240f1faaf695330c33391a8742a4a

sha512=44566902af1ef750d901527b4b9f5ef9872cfed88a935fe94a78e5a07692855949fed5d71e6709a19f5bf619cf3640391f393fdfeaa98834e72c35106af460c3

Sourcetype 'a hyp = {

}

Sourcetype info = {

}

Sourcetype 'a reified_goal = {

}

Sourceval map_reified_goal : f:('a -> 'b) -> 'a reified_goal -> 'b reified_goal

Sourcetype 'a goals = {

}

Sourceval map_goals : f:('a -> 'b) -> 'a goals -> 'b goals

Sourcetype reified_pp = Pp.t reified_goal goals

val reify : 
  ppx:(Environ.env -> Evd.evar_map -> EConstr.t -> 'a) ->
  State.Proof.t ->
  'a reified_goal goals

Stm-independent goal processor