diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/Cstrategy.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 2f731068..28c8eeb8 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -16,6 +16,7 @@ (** A deterministic evaluation strategy for C. *) Require Import Axioms. +Require Import Classical. Require Import Coqlib. Require Import Errors. Require Import Maps. @@ -433,8 +434,6 @@ Proof. intros. eapply star_plus_trans; eauto. apply H1. eapply safe_steps; eauto. auto. Qed. -Require Import Classical. - Lemma safe_imm_safe: forall f C a k e m K, safe (ExprState f (C a) k e m) -> |