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
val hash : t -> intval mode : st:t -> Pvernac.proof_mode optionval parsing : st:t -> Vernacstate.Parser.tmodule Proof : sig ... endProof states
val in_state : st:t -> f:('a -> 'b) -> 'a -> ('b, Loc.t) Protect.E.tExecute a command in state st. Unfortunately this can produce anomalies as Coq state setting is imperative, so we need to wrap it in protect.
val marshal_in : Stdlib.in_channel -> tExtra / interanl
val marshal_out : Stdlib.out_channel -> t -> unitval of_coq : Vernacstate.t -> tval to_coq : t -> Vernacstate.t