From 24a8dbb62e8171f3f3ad87e8d3f697e726df0e6a Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 18 Aug 2009 06:19:46 +0000 Subject: "val_match_approx_increasing" moved from mach-dep part to mach-indep part. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1128 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/ConstpropOpproof.v | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'arm/ConstpropOpproof.v') diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 70fc606c..bb9caffb 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/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 -- cgit