diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-07 21:34:14 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-07 21:34:14 +0200 |
| commit | 249482aed76d209ff203f9afeeb3f10db004e8c0 (patch) | |
| tree | 80efa32a68a7b993ef94751e38acb4b49f849b7d /cfrontend | |
| parent | 5a3d4adc631f5b5d3dc4585b7b28ea18b6faf633 (diff) | |
| download | compcert-kvx-249482aed76d209ff203f9afeeb3f10db004e8c0.tar.gz compcert-kvx-249482aed76d209ff203f9afeeb3f10db004e8c0.zip | |
start implementing expect as expr
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 1 |
1 files changed, 1 insertions, 0 deletions
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. |