diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-04-03 17:45:15 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-04-03 17:45:15 +0200 |
| commit | 8d4562d4d3bebb9c62374beaf39d8327acdc647d (patch) | |
| tree | 186d72ff2c1c9a420dc24d1a7e54c7802e7bf988 /powerpc/Op.v | |
| parent | 0b4bcebe701b9cf8756f583768831ad48a7cc79e (diff) | |
| download | compcert-kvx-8d4562d4d3bebb9c62374beaf39d8327acdc647d.tar.gz compcert-kvx-8d4562d4d3bebb9c62374beaf39d8327acdc647d.zip | |
Replace 'decide equality' in powerpc/Op.v. Bug 21332
Diffstat (limited to 'powerpc/Op.v')
| -rw-r--r-- | powerpc/Op.v | 9 |
1 files changed, 5 insertions, 4 deletions
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}. |