From 249482aed76d209ff203f9afeeb3f10db004e8c0 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 7 Apr 2020 21:34:14 +0200 Subject: start implementing expect as expr --- cfrontend/Cminorgenproof.v | 1 + 1 file changed, 1 insertion(+) (limited to 'cfrontend') diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 5acb996d..744df818 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1335,6 +1335,7 @@ Lemma eval_binop_compat: /\ Val.inject f v tv. Proof. destruct op; simpl; intros; inv H. +- TrivialExists. apply Val.normalize_inject; auto. - TrivialExists. apply Val.add_inject; auto. - TrivialExists. apply Val.sub_inject; auto. - TrivialExists. inv H0; inv H1; constructor. -- cgit