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. --- plugins/funind/Recdef.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/Recdef.v') diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v index e4433247b4..c6fcd647ff 100644 --- a/plugins/funind/Recdef.v +++ b/plugins/funind/Recdef.v @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Import Coq.funind.FunInd. Require Import PeanoNat. - Require Compare_dec. Require Wf_nat. -- cgit v1.2.3 From 930662915d75af750db7da1043f9feda321095b3 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 13 Jun 2017 12:04:34 +0200 Subject: Recdef do now a Require Export FunInd (better compat) --- plugins/funind/Recdef.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/Recdef.v') diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v index c6fcd647ff..64f43b8335 100644 --- a/plugins/funind/Recdef.v +++ b/plugins/funind/Recdef.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Coq.funind.FunInd. +Require Export Coq.funind.FunInd. Require Import PeanoNat. Require Compare_dec. Require Wf_nat. -- cgit v1.2.3