diff options
| author | Pierre-Marie Pédrot | 2021-01-14 19:12:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-14 19:12:11 +0100 |
| commit | eb25e63d58555a67b74a046b8bdf2ab6252164c0 (patch) | |
| tree | b3deef1089255b400e66cb540c315d629aff4108 /engine/proofview.ml | |
| parent | b8a3ebaa9695596f062298f5913ae4f4debb0124 (diff) | |
| parent | 00a09f2cc4a8f4b6baeca0a474e5ab4062ff0f97 (diff) | |
Merge PR #13378: Add support for high resolution timeout functions
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index b3061eaa81..abc1a907d3 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -927,7 +927,7 @@ let _ = CErrors.register_handler begin function | _ -> None end -let tclTIMEOUT n t = +let tclTIMEOUTF n t = let open Proof in (* spiwack: as one of the monad is a continuation passing monad, it doesn't force the computation to be threaded inside the underlying @@ -952,6 +952,8 @@ let tclTIMEOUT n t = return res | Util.Inr (e, info) -> tclZERO ~info e +let tclTIMEOUT n t = tclTIMEOUTF (float_of_int n) t + let tclTIME s t = let pr_time t1 t2 n msg = let msg = |