| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
This has no effect anymore, verbose printing is controlled now by
the regular, common `quiet` flag.
|
|
|
|
|
|
|
|
Now it is a private field, locations are optional.
|
|
It used to be Stateid.initial by default. That is indeed a valid
state id but very likely not the very best one (that would be
the tip of the document).
|
|
Dag extended to support arbitrary clusters, renamed to Property.
Vcs generalized to not impose the data hold by a Property.
Stm(VCS) names a property "a box" and imposes a topological invariant (no
overlap). It defines 2 kind of boxes: ProofTasks (the old cluster
notion) and ErrorBound (meant to confine errors to sub-proofs).
In the meanwhile more equations added to Make(..) functors in order to
have just one Stateid.Set module around.
|
|
This eases the task of replacing/improving the serializer, as well as
making it more resistant. See pitfalls below:
Main changes are:
- fold `message` type into `feedback` type
- make messages of type `Richpp.richpp` so we are explicit about the
content being a rich document.
- moved serialization functions for messages and stateid to `Xmlprotocol`
- improved a couple of internal API points (`is_message`).
Tested.
|
|
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(this should have been the first commit of Paral-ITP)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16688 85f007b7-540e-0410-9357-904b9bb8a0f7
|
