diff options
author | Sigurd Schneider <sigurd.schneider@cs.uni-saarland.de> | 2017-07-20 11:10:00 +0200 |
---|---|---|
committer | Sigurd Schneider <sigurd.schneider@cs.uni-saarland.de> | 2017-07-20 11:20:52 +0200 |
commit | b26b8d219230ae912e3860dc906d34169af2a5c8 (patch) | |
tree | acb660fe64b791e5999a24cf844cc83567c68557 /backend/Allocproof.v | |
parent | 2a78e5fd2f2c70fdd20048b3e23162ad97b2b2b6 (diff) | |
download | compcert-b26b8d219230ae912e3860dc906d34169af2a5c8.tar.gz compcert-b26b8d219230ae912e3860dc906d34169af2a5c8.zip |
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.
Diffstat (limited to 'backend/Allocproof.v')
-rw-r--r-- | backend/Allocproof.v | 1 |
1 files changed, 1 insertions, 0 deletions
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. |