From 8d4562d4d3bebb9c62374beaf39d8327acdc647d Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 3 Apr 2017 17:45:15 +0200 Subject: Replace 'decide equality' in powerpc/Op.v. Bug 21332 --- powerpc/Op.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Op.v b/powerpc/Op.v index d59afd97..e171c7d4 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -24,6 +24,7 @@ syntax and dynamic semantics of the Cminor language. *) +Require Import BoolEqual. Require Import Coqlib. Require Import AST. Require Import Integers. @@ -138,13 +139,13 @@ Proof. decide equality. Defined. +Definition beq_operation: forall (x y: operation), bool. + generalize Int.eq_dec Ptrofs.eq_dec ident_eq Float.eq_dec Float32.eq_dec eq_condition; boolean_equality. +Defined. Definition eq_operation (x y: operation): {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Ptrofs.eq_dec ident_eq; intro. - generalize Float.eq_dec Float32.eq_dec; intros. - generalize eq_condition; intro. - decide equality. + decidable_equality_from beq_operation. Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. -- cgit