package coq-lsp
-
coq-lsp.lsp
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package coq-lsp
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type 'a goals = {goals : 'a list;stack : ('a list * 'a list) list;bullet : Pp.t option;shelf : 'a list;given_up : 'a list;
}type reified_pp = Pp.t reified_goal goalsval reify :
ppx:(Environ.env -> Evd.evar_map -> EConstr.t -> 'a) ->
State.Proof.t ->
'a reified_goal goalsStm-independent goal processor