Module Fleche.Theory

module Check : sig ... end
val create : io:Io.CallBack.t -> token:Coq.Limits.Token.t -> env:Doc.Env.t -> uri:Lang.LUri.File.t -> raw:string -> version:int -> unit

Create a document inside a theory

val 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

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

Close a document

module Request : sig ... end
module Register : sig ... end