From ec94edf830ff9676c43c86f0eb9038c4bd205f62 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 15 Jul 2014 15:46:48 +0200
Subject: Using the generic timeout function in the boostrapped file.

---
 bootstrap/Monads.v | 19 +------------------
 1 file changed, 1 insertion(+), 18 deletions(-)

(limited to 'bootstrap')

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.
-- 
cgit v1.2.3