From 466e6a97c97e83679d49f0867d8f571402e1548f Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 23 Mar 2017 14:42:24 +0100
Subject: extract "plugins/micromega/micromega.ml{,i}" files from
 "plugins/micromega/MExtraction.v"

---
 plugins/micromega/MExtraction.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/micromega/MExtraction.v')

diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index d28bb82863..c976aeb372 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -48,7 +48,7 @@ Extract Constant Rmult => "( * )".
 Extract Constant Ropp  => "fun x -> - x".
 Extract Constant Rinv   => "fun x -> 1 / x".
 
-Extraction "micromega.ml"
+Extraction "plugins/micromega/micromega.ml"
   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 7fff12d45c4d86fa5cb9be3883084ffef5911405 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 30 May 2017 20:04:31 -0400
Subject: Break circular dependency in MExtraction

Described in https://github.com/coq/coq/pull/515#discussion_r119230833
---
 plugins/micromega/MExtraction.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/micromega/MExtraction.v')

diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index c976aeb372..4d5c3b1d5b 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -38,11 +38,11 @@ Extract Inductive sumor => option [ Some None ].
     Let's rather use the ocaml && *)
 Extract Inlined Constant andb => "(&&)".
 
-Require Import Reals.
+Import Reals.Rdefinitions.
 
-Extract Constant R => "int".  
-Extract Constant R0 => "0".  
-Extract Constant R1 => "1".  
+Extract Constant R => "int".
+Extract Constant R0 => "0".
+Extract Constant R1 => "1".
 Extract Constant Rplus => "( + )".
 Extract Constant Rmult => "( * )".
 Extract Constant Ropp  => "fun x -> - x".
-- 
cgit v1.2.3