From 27c8e30fad95d887b698b0e3fa563644c293b033 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 23 Jun 2016 15:07:02 +0200 Subject: 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. --- theories/MSets/MSetAVL.v | 2 +- theories/MSets/MSetGenTree.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/MSets') diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index a3c265a21..b30cb6b56 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -31,7 +31,7 @@ code after extraction. *) -Require Import MSetInterface MSetGenTree BinInt Int. +Require Import FunInd MSetInterface MSetGenTree BinInt Int. Set Implicit Arguments. Unset Strict Implicit. 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. -- cgit v1.2.3