diff options
Diffstat (limited to 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 1d4fb5d39c..6b9d49052d 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -517,10 +517,8 @@ let print x = (** Support for machine floating point values *) -let is_float (x:t) = - let o = Obj.repr x in - Int.equal (Obj.tag o) Obj.double_tag -[@@ocaml.inline always] +external is_float : t -> bool = "coq_is_double" +[@@noalloc] let to_float (x:t) = (Obj.magic x : Float64.t) [@@ocaml.inline always] |