diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 2 | ||||
| -rw-r--r-- | engine/logic_monad.mli | 2 | ||||
| -rw-r--r-- | engine/proofview.ml | 4 | ||||
| -rw-r--r-- | engine/proofview.mli | 3 |
4 files changed, 7 insertions, 4 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 706e51d4b3..ed40b63d14 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -525,7 +525,7 @@ end = struct let principal = if principal then match fgl.principal with - | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.") + | Some _ -> CErrors.user_err Pp.(str "Only one main goal per instantiation.") | None -> Some evk else fgl.principal in diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 7784b38c80..5208469082 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -74,7 +74,7 @@ module NonLogical : sig (** [try ... with ...] but restricted to {!Exception}. *) val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t - val timeout : int -> 'a t -> 'a option t + val timeout : float -> 'a t -> 'a option t (** Construct a monadified side-effect. Exceptions raised by the argument are wrapped with {!Exception}. *) 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 = diff --git a/engine/proofview.mli b/engine/proofview.mli index fe0d7ae51e..bf6021b1b6 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -418,7 +418,8 @@ val tclCHECKINTERRUPT : unit tactic (** [tclTIMEOUT n t] can have only one success. In case of timeout it fails with [tclZERO Tac_Timeout]. *) -val tclTIMEOUT : int -> 'a tactic -> 'a tactic +val tclTIMEOUTF : float -> 'a tactic -> 'a tactic +val tclTIMEOUT : int -> 'a tactic -> 'a tactic (** [tclTIME s t] displays time for each atomic call to t, using s as an identifying annotation if present *) |