aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Op.v
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-03-02 12:13:19 +0100
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-03-02 12:13:19 +0100
commit6bff68d55932bdc4715741a973724317c639b833 (patch)
treec870b860eae3ad62d9e29b0af181368a4035a60a /riscV/Op.v
parentbe4dcbd9fcd3c859a0fae7a37cd226493a8abefb (diff)
downloadcompcert-kvx-6bff68d55932bdc4715741a973724317c639b833.tar.gz
compcert-kvx-6bff68d55932bdc4715741a973724317c639b833.zip
Merge conflicts solved and cleaning in Asmgenproof after expansion
Diffstat (limited to 'riscV/Op.v')
-rw-r--r--riscV/Op.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/riscV/Op.v b/riscV/Op.v
index 4c2390a1..8b4d444d 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -200,8 +200,7 @@ Inductive operation : Type :=
| OEfled (**r compare less-than/equal *)
| OEfeqs (**r compare equal *)
| OEflts (**r compare less-than *)
- | OEfles. (**r compare less-than/equal *)
- | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+ | OEfles (**r compare less-than/equal *)
| Obits_of_single
| Obits_of_float
| Osingle_of_bits