From b125afc697c1214cb329967b506a4a740a942e81 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 12 Mar 2018 09:25:53 +0100
Subject: Do not use "Require" inside sections (#224)

This will soon be deprecated by Coq.

Manual merge of pull request #224 by vbgl.  Closes: #224
---
 cfrontend/Cstrategy.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'cfrontend')

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) ->
-- 
cgit