Support for indirect symbols under MacOS X (final).

Remove stdio hack in runtime/


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1979 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 0 insertions, 13 deletions

diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index 0643296..ff5044f 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -145,19 +145,6 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | _, _ => Unknown
   end.
 
-(** * Generation of constants *)
-
-Parameter generate_float_constants : unit -> bool.
-
-Definition const_for_result (a: approx) : option operation :=
-  match a with
-  | I n => Some(Ointconst n)
-  | F n => if generate_float_constants tt then Some(Ofloatconst n) else None
-  | G symb ofs => Some(Olea (Aglobal symb ofs))
-  | S ofs => Some(Olea (Ainstack ofs))
-  | _ => None
-  end.
-
 (** * Operator strength reduction *)
 
 (** We now define auxiliary functions for strength reduction of