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. --- backend/Allocproof.v | 1 + 1 file changed, 1 insertion(+) (limited to 'backend/Allocproof.v') 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. -- cgit