Module Fleche.TheorySource

Sourcemodule Check : sig ... end
Sourceval open_ : io:Io.CallBack.t -> token:Coq.Limits.Token.t -> env:Doc.Env.t -> uri:Lang.LUri.File.t -> languageId:string -> raw:string -> version:int -> unit

Open a document inside a theory

Sourceval change : io:Io.CallBack.t -> token:Coq.Limits.Token.t -> uri:Lang.LUri.File.t -> version:int -> raw:string -> Int.Set.t

Update a document inside a theory, returns the list of not valid requests

Sourceval close : uri:Lang.LUri.File.t -> unit

Close a document

Sourcemodule Request : sig ... end
Sourcemodule Register : sig ... end