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