diff options
Diffstat (limited to 'backend/RTLgenproof.v')
| -rw-r--r-- | backend/RTLgenproof.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 072db138..b003eb10 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -12,7 +12,7 @@ (** Correctness proof for RTL generation. *) -Require Import Coqlib Maps AST Linking. +Require Import Wellfounded Coqlib Maps AST Linking. Require Import Integers Values Memory Events Smallstep Globalenvs. Require Import Switch Registers Cminor Op CminorSel RTL. Require Import RTLgen RTLgenspec. @@ -1147,8 +1147,6 @@ Qed. Ltac Lt_state := apply lt_state_intro; simpl; try omega. -Require Import Wellfounded. - Lemma lt_state_wf: well_founded lt_state. Proof. |