aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.mllib
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2016-05-31 12:16:40 +0200
committerEmilio Jesus Gallego Arias2016-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 92b3a869a9..bd792b01f6 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -7,6 +7,5 @@ Vernac_classifier
Lemmas
CoqworkmgrApi
AsyncTaskQueue
-Texmacspp
Stm
Vio_checking