aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ssr/ssrfun.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index f77f7c4fa..3aabff824 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -163,7 +163,7 @@ Require Import ssreflect.
(* 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. *)
(* Note that familiar "cancellation" identities like x + y - y = x or *)
-(* x - y + x = x are respectively instances of right_loop and rev_right_loop *)
+(* 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. *)
(* *)
(* - Morphisms for functions and relations: *)