Le dim. 2 déc. 2018 à 02:50, Emilio Jesús Gallego Arias <e...@x80.org> a écrit :
> Pierre Courtieu <pierre.court...@cnam.fr> writes: > > > I think the most important is that your documentation should contain or > > point to a documentation of coq stm. > > Why? I'd rather document SerAPI by itself, why to expose the low-level > document manager? > > Note that the README is not accurate anymore, as SerAPI is not tied to > the STM anymore, so yeah this may be confusing. Does serapi avoids being based on a notion of document model? Last I checked about stm it was based on an implicit DAG roughly representing the lemmas of the file. Don't we need something like that to use serapi correctly? I've already wrote a fair chunk of up-to-date documentation for it, > hopefully will make it into the main branch soon. Cool! > Cheers, > E. >
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
