diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-05-24 10:10:14 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-05-24 10:10:14 +0200 |
| commit | 8d3dbd3636fbb6a056f5506be8ee2d8839c1aea2 (patch) | |
| tree | bc1cb43e67fcfc7d1d1369e39936a5e78093c77c /ia32 | |
| parent | 4e2fb826bd95e3f32459f1845948f37add3cbdb9 (diff) | |
| download | compcert-8d3dbd3636fbb6a056f5506be8ee2d8839c1aea2.tar.gz compcert-8d3dbd3636fbb6a056f5506be8ee2d8839c1aea2.zip | |
ia32/Conventions1: remove commented-out proof attempt
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/Conventions1.v | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/ia32/Conventions1.v b/ia32/Conventions1.v index 672b4219..08a86815 100644 --- a/ia32/Conventions1.v +++ b/ia32/Conventions1.v @@ -213,23 +213,6 @@ Proof. apply size_arguments_rec_above. Qed. -(* -Lemma loc_arguments_bounded: - forall (s: signature) (p: rpair loc), - In p (loc_arguments s) -> - forall_rpair - (fun l => match l with S Outgoing ofs ty => ofs + typesize ty <= size_arguments s | _ => True end) - p. -Proof. - intros until p. unfold loc_arguments, size_arguments. generalize (sig_args s) 0. - induction l as [ | ty l]; simpl; intros x IN. -- contradiction. -- destruct IN as [EQ|IN]. -+ generalize (size_arguments_rec_above l (x + typesize ty)); intros A. - subst p. destruct ty; simpl in *; omega. -+ apply IHl; auto. -Qed. -*) Lemma loc_arguments_bounded: forall (s: signature) (ofs: Z) (ty: typ), In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) -> |