diff options
| author |  fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-20 17:01:54 +0000 |
|---|---|---|
| committer | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-20 17:01:54 +0000 |
| commit | 7da3e3d85c88eb42e932230048cb0db255474b5d (patch) | |
| tree | 0cd987e72b528d88c5a2a6bbcfa1d0718a74efa6 /plugins/micromega/MExtraction.v | |
| parent | 4c6c284ddc6db47f070026ad68b5c29f6737c4a0 (diff) | |
added support to handle division by a constant over R
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14147 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega/MExtraction.v')
| -rw-r--r-- | plugins/micromega/MExtraction.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 9b55eea45..19a98f876 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -38,11 +38,24 @@ 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 N_of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. + + + (* Local Variables: *) (* coding: utf-8 *) (* End: *) |