diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-23 15:07:02 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-14 12:02:35 +0200 |
| commit | 27c8e30fad95d887b698b0e3fa563644c293b033 (patch) | |
| tree | 021febbccb12aff7873cf18aebaf4e9e2a6e4d47 /theories/FSets | |
| 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/FSets')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FMapFullAVL.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FMapList.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FMapWeakList.v | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index c9e5b8dd2..4a790296b 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -16,7 +16,7 @@ See the comments at the beginning of FSetAVL for more details. *) -Require Import FMapInterface FMapList ZArith Int. +Require Import FunInd FMapInterface FMapList ZArith Int. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index a7be32328..b8e362f15 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -25,7 +25,7 @@ *) -Require Import Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega. +Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 5acdb7eb7..aadef476d 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -12,7 +12,7 @@ [FMapInterface.S] using lists of pairs ordered (increasing) with respect to left projection. *) -Require Import FMapInterface. +Require Import FunInd FMapInterface. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 130cbee87..812409702 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -11,7 +11,7 @@ (** This file proposes an implementation of the non-dependent interface [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *) -Require Import FMapInterface. +Require Import FunInd FMapInterface. Set Implicit Arguments. Unset Strict Implicit. |