diff options
Diffstat (limited to 'backend/CSE.v')
| -rw-r--r-- | backend/CSE.v | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index 4347c33..45b50d6 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -57,15 +57,7 @@ Definition eq_valnum: forall (x y: valnum), {x=y}+{x<>y} := peq. Definition eq_list_valnum (x y: list valnum) : {x=y}+{x<>y}. Proof. - induction x; intros; case y; intros. - left; auto. - right; congruence. - right; congruence. - case (eq_valnum a v); intros. - case (IHx l); intros. - left; congruence. - right; congruence. - right; congruence. + decide equality. apply eq_valnum. Qed. Definition eq_rhs (x y: rhs) : {x=y}+{x<>y}. |