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 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. |