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.

15 files changed, 15 insertions, 3 deletions

diff --git a/arm/CombineOpproof.v b/arm/CombineOpproof.v
index cb30e956..820f4b91 100644
--- a/arm/CombineOpproof.v
+++ b/arm/CombineOpproof.v
@@ -13,6 +13,7 @@
 (** Recognition of combined operations, addressing modes and conditions
   during the [CSE] phase. *)
 
+Require Import FunInd.
 Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 6c10d27f..29dbcbe8 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -13,6 +13,7 @@
 (** Correctness proof for the [Allocation] pass (validated translation from
   RTL to LTL). *)
 
+Require Import FunInd.
 Require Import FSets.
 Require Import Coqlib Ordered Maps Errors Integers Floats.
 Require Import AST Linking Lattice Kildall.
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 07c3f84a..28ca27fa 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -12,6 +12,7 @@
 
 (** Elimination of unneeded computations over RTL: correctness proof. *)
 
+Require Import FunInd.
 Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
 Require Import AST Linking.
 Require Import Values Memory Globalenvs Events Smallstep.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index ebc64c6f..69480013 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -12,6 +12,7 @@
 
 (** Correctness of instruction selection *)
 
+Require Import FunInd.
 Require Import Coqlib Maps.
 Require Import AST Linking Errors Integers Values Memory Events Globalenvs Smallstep.
 Require Import Switch Cminor Op CminorSel.
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 7c4c0525..08adff2b 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -10,6 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+Require Import FunInd.
 Require Import Coqlib Maps Integers Floats Lattice Kildall.
 Require Import Compopts AST Linking.
 Require Import Values Memory Globalenvs Events.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index f905ffa2..c71b515c 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -10,6 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+Require Import FunInd.
 Require Import Zwf Coqlib Maps Integers Floats Lattice.
 Require Import Compopts AST.
 Require Import Values Memory Globalenvs Events.
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index a9ffcd3d..e063dfc3 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -12,6 +12,7 @@
 
 (** Animating the CompCert C semantics *)
 
+Require Import FunInd.
 Require Import Axioms Classical.
 Require Import String Coqlib Decidableplus.
 Require Import Errors Maps Integers Floats.
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index d85fb271..ee1df409 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -12,6 +12,7 @@
 
 (** Correctness proof for expression simplification. *)
 
+Require Import FunInd.
 Require Import Coqlib Maps Errors Integers.
 Require Import AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
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.
diff --git a/lib/Heaps.v b/lib/Heaps.v
index 65334a38..2a21f88c 100644
--- a/lib/Heaps.v
+++ b/lib/Heaps.v
@@ -21,6 +21,7 @@
     (If an element is already in a heap, inserting it again does nothing.)
 *)
 
+Require Import FunInd.
 Require Import Coqlib.
 Require Import FSets.
 Require Import Ordered.
diff --git a/lib/Intv.v b/lib/Intv.v
index 57d946e3..a11e619b 100644
--- a/lib/Intv.v
+++ b/lib/Intv.v
@@ -18,7 +18,7 @@
 Require Import Coqlib.
 Require Import Zwf.
 Require Coq.Program.Wf.
-Require Recdef.
+Require Import Recdef.
 
 Definition interv : Type := (Z * Z)%type.
 
diff --git a/lib/Parmov.v b/lib/Parmov.v
index 92bba559..ee7422f4 100644
--- a/lib/Parmov.v
+++ b/lib/Parmov.v
@@ -55,7 +55,7 @@
 Require Import Relations.
 Require Import Axioms.
 Require Import Coqlib.
-Require Recdef.
+Require Import Recdef.
 
 Section PARMOV.
 
diff --git a/powerpc/CombineOpproof.v b/powerpc/CombineOpproof.v
index 4883876d..cca7606a 100644
--- a/powerpc/CombineOpproof.v
+++ b/powerpc/CombineOpproof.v
@@ -13,6 +13,7 @@
 (** Recognition of combined operations, addressing modes and conditions
   during the [CSE] phase. *)
 
+Require Import FunInd.
 Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
diff --git a/riscV/CombineOpproof.v b/riscV/CombineOpproof.v
index 6843da29..a24de1e5 100644
--- a/riscV/CombineOpproof.v
+++ b/riscV/CombineOpproof.v
@@ -13,6 +13,7 @@
 (** Recognition of combined operations, addressing modes and conditions
   during the [CSE] phase. *)
 
+Require Import FunInd.
 Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
diff --git a/x86/CombineOpproof.v b/x86/CombineOpproof.v
index a7024501..69abbf61 100644
--- a/x86/CombineOpproof.v
+++ b/x86/CombineOpproof.v
@@ -13,6 +13,7 @@
 (** Recognition of combined operations, addressing modes and conditions
   during the [CSE] phase. *)
 
+Require Import FunInd.
 Require Import Coqlib.
 Require Import Integers Values Memory.
 Require Import Op RTL CSEdomain.