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