diff options
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 4b75e34d..585fb0da 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 12c05cc3..199ac922 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 86d7ff21..dc01ad20 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 674bc065..3c3aecfd 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 d7eaa228..7cf947ba 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. |