aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/vernacinterp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index e5971e1aaa..3a8a80d25a 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -82,7 +82,7 @@ let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b =
match !default_timeout, timeout with
| _, Some n
| Some n, None ->
- (match Control.timeout n f x with
+ (match Control.timeout (float_of_int n) f x with
| None -> Exninfo.iraise (Exninfo.capture CErrors.Timeout)
| Some x -> x)
| None, None ->