Changeset 2468 for src/Clight/TypeComparison.ma

Timestamp:

Nov 15, 2012, 6:12:57 PM (7 years ago)

Author:

garnier

Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:

• src/Clight/TypeComparison.ma (modified) (2 diffs)

src/Clight/TypeComparison.ma

@@ -9 +9 @@
 definition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
-definition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
-#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
 
 let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
@@ -19 +17 @@
     match sg_eq_dec sg sg' with [ inl e2 ⇒ inl ???
     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
-    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
-    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
-| Tfloat f ⇒ match t2 return λt'. Sum (Tfloat ? = t') (Tfloat ? ≠ t')  with [ Tfloat f' ⇒
-    match fs_eq_dec f f' with [ inl e1 ⇒ inl ???
     | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     | _ ⇒ inr ?? (nmk ? (λH.?)) ]