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