4 files changed, 0 insertions, 8 deletions
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 4e572277..b6b75abe 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -273,7 +273,6 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
   | cast_case_p2bool =>
       match v with
       | Vint i => Some (Vint (cast_int_int IBool Signed i))
-      | Vptr _ _ => Some (Vint Int.one)
       | _ => None
       end
   | cast_case_l2l =>
@@ -391,7 +390,6 @@ Definition bool_val (v: val) (t: type) : option bool :=
   | bool_case_p =>
       match v with
       | Vint n => Some (negb (Int.eq n Int.zero))
-      | Vptr b ofs => Some true
       | _ => None
       end
   | bool_case_l =>
@@ -426,7 +424,6 @@ Definition sem_notbool (v: val) (ty: type) : option val :=
   | bool_case_p =>
       match v with
       | Vint n => Some (Val.of_bool (Int.eq n Int.zero))
-      | Vptr _ _ => Some Vfalse
       | _ => None
       end
   | bool_case_l =>
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 7f61c657..847e4856 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -333,7 +333,6 @@ Proof.
   econstructor; split. econstructor; eauto with cshm. simpl. eauto. 
   unfold Val.cmpu, Val.cmpu_bool. simpl.
   destruct (Int.eq i Int.zero); simpl; constructor.
-  exists Vtrue; split. econstructor; eauto with cshm. constructor.
 (* long *)
   econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. 
   destruct (Int64.eq i Int64.zero); simpl; constructor. 
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 43d34007..bdeeff2a 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -1390,7 +1390,6 @@ Proof.
   destruct (Float.cmp Ceq f Float.zero); constructor; auto with ty.
   destruct (Float32.cmp Ceq f Float32.zero); constructor; auto with ty.
   destruct (Int.eq i Int.zero); constructor; auto with ty.
-  constructor; auto with ty.
   destruct (Int64.eq i Int64.zero); constructor; auto with ty.
 - (* notint *)
   unfold sem_notint in SEM; DestructCases; auto with ty.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 5cf59d94..3364ec6a 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -267,11 +267,8 @@ Proof.
   constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto.
   constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto.
   constructor. simpl. destruct (Int.eq i Int.zero); auto.
-  constructor; auto.
   constructor. simpl. destruct (Int.eq i Int.zero); auto.
-  constructor; auto.
   constructor. simpl. destruct (Int.eq i Int.zero); auto.
-  constructor; auto.
 (* long *)
   destruct ty; try (destruct f); try discriminate.
   destruct v; inv H. constructor.