aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Anton Trunov <anton.a.trunov@gmail.com>2018-02-13 22:55:01 +0100
committerGravatar Anton Trunov <anton.a.trunov@gmail.com>2018-03-04 19:24:19 +0100
commit5233abd2f876af6b9e5b705b2ab4df8cdb50b12e (patch)
treedc071d2007b80eeaeb33b2b7b8b45fb70b197c8b /plugins
parent78551857a41a57607ecfb3fd010e0a9755f47cea (diff)
ssr: fix typo in doc comment
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: *)