coq-lsp.coq
Coq.Ast
coq-lsp.fleche
coq-lsp.lsp
type t
val loc : t -> Loc.t option
val hash : t -> int
val compare : t -> t -> int
val grab_definitions : (Loc.t -> Names.Id.t -> 'a) -> t list -> 'a list
val print : t -> Pp.t
Printing
val pp_loc : ?print_file:bool -> Format.formatter -> Loc.t -> unit
val loc_to_string : ?print_file:bool -> Loc.t -> string
val marshal_in : in_channel -> t
Unused for now
val marshal_out : out_channel -> t -> unit
val to_coq : t -> Vernacexpr.vernac_control
Internal, will go away once the Lang.t interface is ready
Lang.t
val of_coq : Vernacexpr.vernac_control -> t