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/scheme.ml | 2 ++
 1 file changed, 2 insertions(+)

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

diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index dd840cd929..c341ec8d57 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -131,6 +131,8 @@ let rec pp_expr env args =
     | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
     | MLuint _ ->
       paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
+    | MLfloat _ ->
+      paren (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"")
 
 and pp_cons_args env = function
   | MLcons (_,r,args) when is_coinductive r ->
-- 
cgit v1.2.3