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.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 0a41af45..d28bb828 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -50,7 +50,7 @@ Extract Constant Rinv => "fun x -> 1 / x".
Extraction "micromega.ml"
List.map simpl_cone (*map_cone indexes*)
- denorm Qpower
+ denorm Qpower vm_add
n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.