diff options
Diffstat (limited to 'cfrontend/Ctyping.v')
| -rw-r--r-- | cfrontend/Ctyping.v | 1 |
1 files changed, 0 insertions, 1 deletions
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. |