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')

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