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 | |
| 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')
| -rw-r--r-- | backend/Allocproof.v | 1 | ||||
| -rw-r--r-- | backend/Deadcodeproof.v | 1 | ||||
| -rw-r--r-- | backend/Selectionproof.v | 1 | ||||
| -rw-r--r-- | backend/ValueAnalysis.v | 1 | ||||
| -rw-r--r-- | backend/ValueDomain.v | 1 |
5 files changed, 5 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. 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. |