diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-02 17:01:28 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-02 17:01:28 +0100 |
| commit | 3049b2930ec2bd4adf886fc90bf01a478b318477 (patch) | |
| tree | 00ff808e57abcbc2dcb1775707d26dd9eeba3692 /stm/stm.ml | |
| parent | 57c7d751df85366ba3781c4e1107a745a660714d (diff) | |
Remove some useless module opening.
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index e0e787503..96f127aa2 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1616,7 +1616,7 @@ end = struct (* {{{ *) let vernac_interp switch prev id q = assert(TaskQueue.n_workers (Option.get !queue) > 0); TaskQueue.enqueue_task (Option.get !queue) - QueryTask.({ QueryTask.t_where = prev; t_for = id; t_what = q }, switch) + QueryTask.({ t_where = prev; t_for = id; t_what = q }, switch) let init () = queue := Some (TaskQueue.create (if !Flags.async_proofs_full then 1 else 0)) |