diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-10-07 15:44:20 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-10-07 15:44:20 +0200 |
| commit | 5ffa8534d09272e5f44c51193e74cffdbc2b043c (patch) | |
| tree | c391ce9fa363db667a36775c8cf56a6e6f484ed0 /mppa_k1c | |
| parent | bd4fbff2badea3922bf0e144777ae8ecfdc30e74 (diff) | |
| download | compcert-kvx-5ffa8534d09272e5f44c51193e74cffdbc2b043c.tar.gz compcert-kvx-5ffa8534d09272e5f44c51193e74cffdbc2b043c.zip | |
Icond
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Op.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index f9a774e8..ce9a5dcd 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -51,6 +51,12 @@ Inductive condition : Type := | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) | Cnotcompfs (c: comparison). (**r negation of a floating-point comparison *) +Definition condition_eq: forall (x y: condition), {x = y} + {x <> y}. +Proof. + generalize comparison_eq int_eq int64_eq. + decide equality. +Defined. + Inductive condition0 : Type := | Ccomp0 (c: comparison) (**r signed integer comparison with 0 *) | Ccompu0 (c: comparison) (**r unsigned integer comparison with 0 *) |