aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-23 15:07:02 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-06-14 12:02:35 +0200
commit27c8e30fad95d887b698b0e3fa563644c293b033 (patch)
tree021febbccb12aff7873cf18aebaf4e9e2a6e4d47 /plugins/micromega
parentb240771a3661883ca0cc0497efee5b48519bddea (diff)
Prelude : no more autoload of plugins extraction and recdef
The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
Diffstat (limited to 'plugins/micromega')
-rw-r--r--plugins/micromega/MExtraction.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 135a71520..95f135c8f 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -14,6 +14,7 @@
(* Used to generate micromega.ml *)
+Require Extraction.
Require Import ZMicromega.
Require Import QMicromega.
Require Import RMicromega.