From b26b8d219230ae912e3860dc906d34169af2a5c8 Mon Sep 17 00:00:00 2001 From: Sigurd Schneider 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. --- lib/Heaps.v | 1 + lib/Intv.v | 2 +- lib/Parmov.v | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) (limited to 'lib') 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. -- cgit