From 3cb32772ccd0f2882a40d7f75b044b738adadad3 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 22 Oct 2019 11:57:16 +0200
Subject: Add extraction for primitive floats

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
---
 plugins/extraction/ocaml.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'plugins/extraction/ocaml.ml')

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index e7004fe9af..34ddf57b40 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -307,6 +307,9 @@ let rec pp_expr par env args =
     | MLuint i ->
         assert (args=[]);
         str "(" ++ str (Uint63.compile i) ++ str ")"
+    | MLfloat f ->
+        assert (args=[]);
+        str "(" ++ str (Float64.compile f) ++ str ")"
 
 
 and pp_record_proj par env typ t pv args =
-- 
cgit v1.2.3