From b26b8d219230ae912e3860dc906d34169af2a5c8 Mon Sep 17 00:00:00 2001
From: Sigurd Schneider <sigurd.schneider@cs.uni-saarland.de>
Date: Thu, 20 Jul 2017 11:10:00 +0200
Subject: Ensure FunInd or Recdef is imported if functional induction is used

Coq 8.7 does not load FunInd in prelude anymore, so this is necessary.
Recdef exports FunInd, so if Recdef is imported, importing FunInd
is not required.
---
 common/Globalenvs.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'common/Globalenvs.v')

diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index dd8a1eb9..25830477 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -33,7 +33,7 @@
   place during program linking and program loading in a real operating
   system. *)
 
-Require Recdef.
+Require Import Recdef.
 Require Import Zwf.
 Require Import Axioms Coqlib Errors Maps AST Linking.
 Require Import Integers Floats Values Memory.
-- 
cgit