aboutsummaryrefslogtreecommitdiff
path: root/stm/workerLoop.mli
diff options
context:
space:
mode:
authorMaxime Dénès2017-03-24 16:15:32 +0100
committerMaxime Dénès2017-03-24 16:15:32 +0100
commitaf291869bb7d1184d8e655906572d75937ca829b (patch)
tree62a5ccf9ee7b115b7d1118cbc3db92c553261713 /stm/workerLoop.mli
parent3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (diff)
parent7535e268f7706d1dee263fdbafadf920349103db (diff)
Merge branch 'trunk' into pr379
Diffstat (limited to 'stm/workerLoop.mli')
-rw-r--r--stm/workerLoop.mli9
1 files changed, 9 insertions, 0 deletions
diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli
new file mode 100644
index 0000000000..dcbf9c88d6
--- /dev/null
+++ b/stm/workerLoop.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+val loop : (unit -> unit) -> string list -> string list