You can search for identifiers within the package.
in-package search v0.2.0
vsrocq-language-server.lsp
Protocol.PpProofState
type hypothesis = {
ids : string list;
body : string option;
_type : string;
}
val hypothesis_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> hypothesis
val yojson_of_hypothesis : hypothesis -> Ppx_yojson_conv_lib.Yojson.Safe.t
type goal = {
id : int;
name : string option;
hypotheses : hypothesis list;
goal : string;
val goal_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> goal
val yojson_of_goal : goal -> Ppx_yojson_conv_lib.Yojson.Safe.t
type t = {
goals : goal list;
shelvedGoals : goal list;
givenUpGoals : goal list;
unfocusedGoals : goal list;
val t_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> t
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
module CompactedDecl = ProofState.CompactedDecl
val mk_pp_hyp : Environ.env -> Evd.evar_map -> CompactedDecl.t -> hypothesis
val goal_name : Libnames.full_path -> string
val mk_goal : Environ.env -> Evd.evar_map -> Evar.t -> goal
val proof_of_state : Vernacstate.t -> Proof.t option
val string_of_diff_mode : Settings.Goals.Diff.Mode.t -> string
val set_diff_mode : Settings.Goals.Diff.Mode.t -> unit
val get_proof : Vernacstate.t -> t option