Merge of "newspilling" branch:

- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
  support saving and restoring registers without knowing
  the exact types (int/single/float) of their contents, just
  their sizes.
- Memory model: generalize the opaque encoding of pointers to
  apply to any value, not just pointers, if chunks Many32/Many64
  are selected.
- More properties of FP arithmetic proved.


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

1 files changed, 1 insertions, 2 deletions

diff --git a/backend/CSE.v b/backend/CSE.v
index 373acce..fa22987 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -293,7 +293,6 @@ Definition store_normalized_range (chunk: memory_chunk) : aval :=
   | Mint8unsigned => Uns 8
   | Mint16signed => Sgn 16
   | Mint16unsigned => Uns 16
-  | Mfloat32 => Fsingle
   | _ => Vtop
   end.
 
@@ -380,7 +379,7 @@ Variable n: numbering.
 Fixpoint reduce_rec (niter: nat) (op: A) (args: list valnum) : option(A * list reg) :=
   match niter with
   | O => None
-  | S niter' =>
+  | Datatypes.S niter' =>
       match f (fun v => find_valnum_num v n.(num_eqs)) op args with
       | None => None
       | Some(op', args') =>