aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEnrico Tassi2014-10-30 17:47:07 +0100
committerEnrico Tassi2014-10-31 15:54:00 +0100
commite6afe851f90c8a864c20fe287ee3a7d5e03c8b77 (patch)
tree066a6a28a8493819f1ee02f31d9f8a27bb96f82e
parentbaef2bd34e1906ab56918c37a90c5468a4785656 (diff)
STM: reorganize code and file names
- proofworkertop to deal with proof tasks - tacworkertop to deal with par: tactics - queryworkertop to deal with queries (next commit)
-rw-r--r--Makefile.common2
-rw-r--r--stm/proofworkertop.ml (renamed from stm/stmworkertop.ml)0
-rw-r--r--stm/proofworkertop.mllib1
-rw-r--r--stm/stm.ml2
-rw-r--r--stm/stmworkertop.mllib1
5 files changed, 3 insertions, 3 deletions
diff --git a/Makefile.common b/Makefile.common
index b47a3e3224..297c046135 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -165,7 +165,7 @@ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
parsing/parsing.cma printing/printing.cma tactics/tactics.cma \
stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma
-TOPLOOPCMA:=stm/stmworkertop.cma stm/tacworkertop.cma
+TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma
diff --git a/stm/stmworkertop.ml b/stm/proofworkertop.ml
index 0d1b44e494..0d1b44e494 100644
--- a/stm/stmworkertop.ml
+++ b/stm/proofworkertop.ml
diff --git a/stm/proofworkertop.mllib b/stm/proofworkertop.mllib
new file mode 100644
index 0000000000..f9f6c22d51
--- /dev/null
+++ b/stm/proofworkertop.mllib
@@ -0,0 +1 @@
+Proofworkertop
diff --git a/stm/stm.ml b/stm/stm.ml
index 64cf9bad72..1077b8b2b3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -736,7 +736,7 @@ module Task = struct
| RespBuiltProof of Proof_global.closed_proof_output * float
| RespError of error
- let name = "stmworker"
+ let name = "proofworker"
let extra_env () = !async_proofs_workers_extra_env
let name_of_task t = t.t_name
diff --git a/stm/stmworkertop.mllib b/stm/stmworkertop.mllib
deleted file mode 100644
index 78b54b2ea9..0000000000
--- a/stm/stmworkertop.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Stmworkertop