diff options
Diffstat (limited to 'bootstrap')
| -rw-r--r-- | bootstrap/Monads.v | 19 |
1 files changed, 1 insertions, 18 deletions
diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v index a029df3147..d0412827b1 100644 --- a/bootstrap/Monads.v +++ b/bootstrap/Monads.v @@ -235,24 +235,7 @@ Module IOBase. Extract Constant print => "fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> let e = Errors.push e in raise e ()". Parameter timeout: forall A, Int -> T A -> T A. - Extract Constant timeout => "fun n t -> (); fun () -> - let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in - let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in - Pervasives.ignore (Unix.alarm n); - let restore_timeout () = - Pervasives.ignore (Unix.alarm 0); - Sys.set_signal Sys.sigalrm psh - in - try - let res = t () in - restore_timeout (); - res - with - | e -> - let e = Errors.push e in - restore_timeout (); - Pervasives.raise e - ". + Extract Constant timeout => "fun n t -> (); fun () -> Control.timeout n t (Proof_errors.Exception Proof_errors.Timeout)". Extraction Implicit timeout [A]. End IOBase. |