diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-25 10:32:38 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-25 10:32:38 +0200 |
| commit | bb185aa85ddf32feed61d7888c1b199fffdd821f (patch) | |
| tree | 04b9489a4ad344b635f958eefba2126709d10cf7 /mppa_k1c/Op.v | |
| parent | b66d6034fb09e6129ca24dd458fbef49e4cb98d7 (diff) | |
| download | compcert-kvx-bb185aa85ddf32feed61d7888c1b199fffdd821f.tar.gz compcert-kvx-bb185aa85ddf32feed61d7888c1b199fffdd821f.zip | |
IT COMPILES
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 8180c43f..8293af1e 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -198,7 +198,7 @@ Inductive operation : Type := | Oselectl (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) | Oselectf (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) | Oselectfs (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) - | Oextfz (stop : int) (start : int). + | Oextfz (stop : Z) (start : Z). (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -233,7 +233,7 @@ Defined. Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0; intros. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0 Z.eq_dec; intros. decide equality. Defined. |