aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.mllib
Commit message (Collapse)AuthorAge
* [xml] Restore protocol compatibility with 8.6.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | By default, we serialize messages to the "rich printing representation" as it was done in 8.6, this ways clients don't have to adapt unless they specifically request the new format using option `--xml_format=Ppcmds`
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
| | | | | | | | | | | | | | | | | | Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.
* STM: proof block detection for bullets and { block }Gravatar Enrico Tassi2016-06-06
|
* Move serialization functions out of StmGravatar Emilio Jesus Gallego Arias2016-06-02
| | | | | | | | | Serialization should be specific to each particular backend, so we let the Stm clients choose how the send the nodes. This should be quite safe to pull in. Test suite passes. Related to #180
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
|
* XML pretty printing for AST (work by François Poulain, project DoCoq)Gravatar Enrico Tassi2014-09-29
| | | | It is not 100% complete, but the main part is there.
* coqworkmgrGravatar Enrico Tassi2014-09-02
|
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
|
* Adding a stm/ folder, as asked during last workgroup. It was essentially movingGravatar Pierre-Marie Pédrot2014-04-25
files around. A bunch of files from lib/ that were only used in the STM were moved, as well as part of toplevel/ related to the STM.