summaryrefslogtreecommitdiff
path: root/plugins/micromega/MExtraction.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/MExtraction.v')
-rw-r--r--plugins/micromega/MExtraction.v19
1 files changed, 16 insertions, 3 deletions
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 5afe7e37..64181cde 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -23,7 +23,7 @@ Require Import NArith.
Require Import QArith.
Extract Inductive prod => "( * )" [ "(,)" ].
-Extract Inductive List.list => list [ "[]" "(::)" ].
+Extract Inductive list => list [ "[]" "(::)" ].
Extract Inductive bool => bool [ true false ].
Extract Inductive sumbool => bool [ true false ].
Extract Inductive option => option [ Some None ].
@@ -38,10 +38,23 @@ Extract Inductive sumor => option [ Some None ].
Let's rather use the ocaml && *)
Extract Inlined Constant andb => "(&&)".
+Require Import Reals.
+
+Extract Constant R => "int".
+Extract Constant R0 => "0".
+Extract Constant R1 => "1".
+Extract Constant Rplus => "( + )".
+Extract Constant Rmult => "( * )".
+Extract Constant Ropp => "fun x -> - x".
+Extract Constant Rinv => "fun x -> 1 / x".
+
Extraction "micromega.ml"
List.map simpl_cone (*map_cone indexes*)
denorm Qpower
- n_of_Z Nnat.N_of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+
+
+
(* Local Variables: *)
(* coding: utf-8 *)