diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-20 11:30:21 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-20 11:30:21 +0100 |
| commit | 7bd5d66520bfae2bdef6573a40798a5d6375be79 (patch) | |
| tree | 86fbe49fed5ead01ca2d8e0d4e163b819ce40bfa /backend/SplitLongproof.v | |
| parent | 84af0898061f8689a84041acc309d63379389366 (diff) | |
| download | compcert-kvx-7bd5d66520bfae2bdef6573a40798a5d6375be79.tar.gz compcert-kvx-7bd5d66520bfae2bdef6573a40798a5d6375be79.zip | |
Proving eval_divs_base
Diffstat (limited to 'backend/SplitLongproof.v')
| -rw-r--r-- | backend/SplitLongproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index 3b74b216..a74276c7 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -313,7 +313,7 @@ Theorem eval_longofint: unary_constructor_sound longofint Val.longofint. Proof. red; intros. unfold longofint. destruct (longofint_match a). - InvEval. econstructor; split. apply eval_longconst. auto. -- exploit (eval_shrimm ge sp e m (Int.repr 31) (x :: le) (Eletvar 0)). EvalOp. +- exploit (eval_shrimm prog sp e m (Int.repr 31) (x :: le) (Eletvar 0)). EvalOp. intros [v1 [A B]]. econstructor; split. EvalOp. destruct x; simpl; auto. |