From 22ee3faf16e9d9f528f4738d562892e9c4d653b5 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 30 Oct 2019 12:04:22 +0100
Subject: Add some doc snippet in ExtrOCamlFloats.v

(as suggested by @silene)
---
 plugins/extraction/ExtrOCamlFloats.v | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/ExtrOCamlFloats.v b/plugins/extraction/ExtrOCamlFloats.v
index 1b07215c63..1891772cc2 100644
--- a/plugins/extraction/ExtrOCamlFloats.v
+++ b/plugins/extraction/ExtrOCamlFloats.v
@@ -8,7 +8,18 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Extraction to OCaml of native binary64 floating-point numbers. *)
+(** Extraction to OCaml of native binary64 floating-point numbers.
+
+Note: the extraction of primitive floats relies on Coq's internal file
+kernel/float64.ml, so make sure the corresponding binary is available
+when linking the extracted OCaml code.
+
+For example, if you build a (_CoqProject + coq_makefile)-based project
+and if you created an empty subfolder "extracted" and a file "test.v"
+containing [Cd "extracted". Separate Extraction function_to_extract.],
+you will just need to add in the _CoqProject: [test.v], [-I extracted]
+and the list of [extracted/*.ml] and [extracted/*.mli] files, then add
+[CAMLFLAGS += -w -33] in the Makefile.local file.  *)
 
 From Coq Require Floats Extraction.
 
-- 
cgit v1.2.3