From b240771a3661883ca0cc0497efee5b48519bddea Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 14 Jun 2017 11:46:40 +0200
Subject: Makefile.build : cleanup now that micromega.ml isn't generated + sync
 check of this file

 There is now a warning if the content of micromega.ml isn't what MExtraction.v would
 produce.
---
 plugins/micromega/MExtraction.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins/micromega')

diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 2451aeada7..135a715203 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -48,7 +48,10 @@ Extract Constant Rmult => "( * )".
 Extract Constant Ropp  => "fun x -> - x".
 Extract Constant Rinv   => "fun x -> 1 / x".
 
-Extraction "plugins/micromega/generated_micromega.ml"
+(** We now extract to stdout, see comment in Makefile.build *)
+
+(*Extraction "plugins/micromega/micromega.ml" *)
+Recursive Extraction
   List.map simpl_cone (*map_cone  indexes*)
   denorm Qpower vm_add
   n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
-- 
cgit v1.2.3


From 27c8e30fad95d887b698b0e3fa563644c293b033 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Thu, 23 Jun 2016 15:07:02 +0200
Subject: Prelude : no more autoload of plugins extraction and recdef

 The user now has to manually load them, respectively via:
   Require Extraction
   Require Import FunInd

 The "Import" in the case of FunInd is to ensure that the
 tactics functional induction and functional inversion are indeed
 in scope.

 Note that the Recdef.v file is still there as well (it contains
 complements used when doing Function with measures), and it also
 triggers a load of FunInd.v.

 This change is correctly documented in the refman, and the test-suite
 has been adapted.
---
 plugins/micromega/MExtraction.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/micromega')

diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 135a715203..95f135c8f0 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -14,6 +14,7 @@
 
 (* Used to generate micromega.ml *)
 
+Require Extraction.
 Require Import ZMicromega.
 Require Import QMicromega.
 Require Import RMicromega.
-- 
cgit v1.2.3