diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/ConstpropOpproof.v | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index c9d77143..0c7be7bd 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -47,17 +47,6 @@ Definition val_match_approx (a: approx) (v: val) : Prop := | _ => False end. -Lemma val_match_approx_increasing: - forall a1 a2 v, - Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v. -Proof. - intros until v. - intros [A|[B|C]]. - subst a1. simpl. auto. - subst a2. simpl. tauto. - subst a2. auto. -Qed. - Inductive val_list_match_approx: list approx -> list val -> Prop := | vlma_nil: val_list_match_approx nil nil |