diff options
| author | Enrico Tassi | 2014-10-30 17:47:07 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-31 15:54:00 +0100 |
| commit | e6afe851f90c8a864c20fe287ee3a7d5e03c8b77 (patch) | |
| tree | 066a6a28a8493819f1ee02f31d9f8a27bb96f82e | |
| parent | baef2bd34e1906ab56918c37a90c5468a4785656 (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.common | 2 | ||||
| -rw-r--r-- | stm/proofworkertop.ml (renamed from stm/stmworkertop.ml) | 0 | ||||
| -rw-r--r-- | stm/proofworkertop.mllib | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 2 | ||||
| -rw-r--r-- | stm/stmworkertop.mllib | 1 |
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 |
