diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-25 15:11:30 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-25 15:11:30 +0200 |
| commit | 1f004665758e26e6e48d13f5702fe55af8944448 (patch) | |
| tree | e3ccaee73c86ec1aef94ef66341610ed4436f93a /backend/SplitLongproof.v | |
| parent | 271a6f98809fbeac6cb04fb29fccbcf9c1e18335 (diff) | |
| download | compcert-kvx-1f004665758e26e6e48d13f5702fe55af8944448.tar.gz compcert-kvx-1f004665758e26e6e48d13f5702fe55af8944448.zip | |
Update ARM port. Not tested yet.
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 31f5db67..07759dc9 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -791,7 +791,7 @@ Proof. Qed. Lemma eval_mullimm: - forall n, unary_constructor_sound (fun a => mullimm a n) (fun v => Val.mull v (Vlong n)). + forall n, unary_constructor_sound (mullimm n) (fun v => Val.mull v (Vlong n)). Proof. unfold mullimm; red; intros. predSpec Int64.eq Int64.eq_spec n Int64.zero. |