From 3ec022950ec233a2af418aacd1755fce4d701724 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 19 Feb 2014 09:55:45 +0000
Subject: Add option -Os to optimize for code size rather than for execution
 speed. Refactored compilation flags that affect the Coq part (module
 Compopts). Added support for C99 for loops with declarations.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/ConstpropOp.vp     | 1 +
 arm/ConstpropOpproof.v | 1 +
 arm/ValueAOp.v         | 1 +
 3 files changed, 3 insertions(+)

(limited to 'arm')

diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 0540781..bf08610 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -14,6 +14,7 @@
   and conditions.  This is the machine-dependent part of [Constprop]. *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index ad7dcd1..90e18f2 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -13,6 +13,7 @@
 (** Correctness proof for constant propagation (processor-dependent part). *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v
index c968213..037b22e 100644
--- a/arm/ValueAOp.v
+++ b/arm/ValueAOp.v
@@ -11,6 +11,7 @@
 (* *********************************************************************)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
-- 
cgit v1.2.3