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/Deadcodeproof.v | |
| parent | 2a78e5fd2f2c70fdd20048b3e23162ad97b2b2b6 (diff) | |
| download | compcert-kvx-b26b8d219230ae912e3860dc906d34169af2a5c8.tar.gz compcert-kvx-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/Deadcodeproof.v')
| -rw-r--r-- | backend/Deadcodeproof.v | 1 |
1 files changed, 1 insertions, 0 deletions
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. |