diff options
| author | Maxime Dénès | 2017-12-27 10:19:21 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-27 10:19:21 +0100 |
| commit | 4969f9425cb0d5cd5bd735110886a0cbd2641588 (patch) | |
| tree | 6c05276df78dd476642ab5db8437e8730d19eb56 /lib/cThread.mli | |
| parent | 3921ff2e2c189063ec46f54cbb247570b6c59b2c (diff) | |
| parent | 5ffa147bd2fe548df3ac9053fe497d0871a5f6df (diff) | |
Merge PR #6444: [lib] Split auxiliary libraries into Coq-specific and general.
Diffstat (limited to 'lib/cThread.mli')
| -rw-r--r-- | lib/cThread.mli | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/lib/cThread.mli b/lib/cThread.mli deleted file mode 100644 index 66f039bb52..0000000000 --- a/lib/cThread.mli +++ /dev/null @@ -1,26 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* As of OCaml 4.01.0 input_value and input do not quite work well - * with threads. The symptom is the following. Two threads, each - * of them blocked on a read (on different channels). One is not - * woken up even if data is available. When the other one gets data - * then the stuck one is eventually unblocked too. Unix.select with - * an unbounded wait has the same problem. *) - -(* Use only the following functions on the channel *) -type thread_ic -val prepare_in_channel_for_thread_friendly_io : in_channel -> thread_ic - -val thread_friendly_input_value : thread_ic -> 'a -val thread_friendly_read : - thread_ic -> Bytes.t -> off:int -> len:int -> int -val thread_friendly_really_read : - thread_ic -> Bytes.t -> off:int -> len:int -> unit -val thread_friendly_really_read_line : thread_ic -> string - |