aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.mllib
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-05-31 12:16:40 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-06-02 16:45:39 +0200
commite020cc70578b65609ac7337537f16a1c25254e77 (patch)
tree3c69737afc2e5693d5ca65b14e169ac406adc187 /stm/stm.mllib
parent2d2d86c165cac7b051da1c5079d614a76550a20c (diff)
Move serialization functions out of Stm
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
Diffstat (limited to 'stm/stm.mllib')
-rw-r--r--stm/stm.mllib1
1 files changed, 0 insertions, 1 deletions
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 92b3a869a..bd792b01f 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -7,6 +7,5 @@ Vernac_classifier
Lemmas
CoqworkmgrApi
AsyncTaskQueue
-Texmacspp
Stm
Vio_checking