diff options
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 22863f451d..abc1a907d3 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -909,10 +909,11 @@ let tclPROGRESS t = in let test = quick_test || + (CList.same_length initial.comb final.comb && Util.List.for_all2eq begin fun i f -> Progress.goal_equal ~evd:initial.solution ~extended_evd:final.solution (drop_state i) (drop_state f) - end initial.comb final.comb + end initial.comb final.comb) in if not test then tclUNIT res @@ -926,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 @@ -951,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 = |