diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-03-12 09:25:53 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-03-12 09:25:53 +0100 |
commit | b125afc697c1214cb329967b506a4a740a942e81 (patch) | |
tree | f42085b4b76bdd9b2987e5077e12eadd6ba5bf95 | |
parent | 96913f741fa9bb31502e32178d67f9efb81033c3 (diff) | |
download | compcert-b125afc697c1214cb329967b506a4a740a942e81.tar.gz compcert-b125afc697c1214cb329967b506a4a740a942e81.zip |
Do not use "Require" inside sections (#224)
This will soon be deprecated by Coq.
Manual merge of pull request #224 by vbgl. Closes: #224
-rw-r--r-- | backend/RTLgenproof.v | 4 | ||||
-rw-r--r-- | cfrontend/Cstrategy.v | 3 |
2 files changed, 2 insertions, 5 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. 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) -> |