Module Fleche.Theory

module Check : sig ... end
val create : io:Io.CallBack.t -> root_state:Coq.State.t -> workspace:Coq.Workspace.t -> uri:Lang.LUri.File.t -> raw:string -> version:int -> unit

Create a document inside a theory

val change : io:Io.CallBack.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