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
---
 ia32/ConstpropOp.vp     | 1 +
 ia32/ConstpropOpproof.v | 1 +
 ia32/ValueAOp.v         | 1 +
 3 files changed, 3 insertions(+)

(limited to 'ia32')

diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index 396c94c..aaf08a1 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -14,6 +14,7 @@
     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/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index d9e6068..148a08d 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -13,6 +13,7 @@
 (** Correctness proof for operator strength reduction. *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v
index 022e015..1802e11 100644
--- a/ia32/ValueAOp.v
+++ b/ia32/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