summaryrefslogtreecommitdiff
path: root/cfrontend/Cshmgenproof2.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Cshmgenproof2.v')
-rw-r--r--cfrontend/Cshmgenproof2.v6
1 files changed, 0 insertions, 6 deletions
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index 1a5eaa0..0458bd5 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -171,12 +171,6 @@ Proof.
intros until m2; intro SEM. unfold make_notbool.
functional inversion SEM; intros; inversion H4; simpl;
eauto with cshm.
- eapply make_binop_correct.
- eapply make_binop_correct. eauto. eauto with cshm.
- simpl; reflexivity. reflexivity. eauto with cshm.
- simpl. rewrite Float.cmp_ne_eq.
- destruct (Float.cmp Ceq f Float.zero); reflexivity.
- traceEq.
Qed.
Lemma make_notint_correct: