diff options
author | 2016-06-23 15:07:02 +0200 | |
---|---|---|
committer | 2017-06-14 12:02:35 +0200 | |
commit | 27c8e30fad95d887b698b0e3fa563644c293b033 (patch) | |
tree | 021febbccb12aff7873cf18aebaf4e9e2a6e4d47 /theories/MSets/MSetGenTree.v | |
parent | b240771a3661883ca0cc0497efee5b48519bddea (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 'theories/MSets/MSetGenTree.v')
-rw-r--r-- | theories/MSets/MSetGenTree.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 154c2384c..036ff1aa4 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -27,7 +27,7 @@ - min_elt max_elt choose *) -Require Import Orders OrdersFacts MSetInterface PeanoNat. +Require Import FunInd Orders OrdersFacts MSetInterface PeanoNat. Local Open Scope list_scope. Local Open Scope lazy_bool_scope. |