coq-lsp.coq
Protect.Error
This modules reifies Coq side effects into an algebraic structure.
This is obviously very convenient for upper layer programming.
As of today this includes feedback and exceptions.
coq-lsp.fleche
coq-lsp.lsp
type payload = Loc.t option * Pp.t
type t = private
| User of payload
| Anomaly of payload