From 7c0352e40af80c222507b1ddcf5e3a2ad29feb67 Mon Sep 17 00:00:00 2001
From: Antonio Nikishaev
Date: Sun, 13 Oct 2019 20:44:04 +0400
Subject: fix rev_right_loop doc

---
 plugins/ssr/ssrfun.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index 0ce3752a51..dc774e811e 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -166,7 +166,7 @@ Require Import ssreflect.
          right_loop inv op <-> op, inv obey the inverse loop right axiom:
                               (x op y) op (inv y) = x for all x, y.
      rev_right_loop inv op <-> op, inv obey the inverse loop reverse right
-                              axiom: (x op y) op (inv y) = x for all x, y.
+                              axiom: (x op (inv y)) op y = x for all x, y.
    Note that familiar "cancellation" identities like x + y - y = x or
  x - y + y = x are respectively instances of right_loop and rev_right_loop
  The corresponding lemmas will use the K and NK/VK suffixes, respectively.
-- 
cgit v1.2.3