From f377960d80f5a31620b1105758b0c24aef828cd3 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Mon, 12 Jun 2017 19:28:52 +0200
Subject: Store plugins/micromega/micromega.{ml,mli} files in the repository.
 Try to generate them later.

---
 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 4d5c3b1d5b..2451aeada7 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 "plugins/micromega/micromega.ml"
+Extraction "plugins/micromega/generated_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