From 930662915d75af750db7da1043f9feda321095b3 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
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 c6fcd647f..64f43b833 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