From 5233abd2f876af6b9e5b705b2ab4df8cdb50b12e Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Tue, 13 Feb 2018 22:55:01 +0100
Subject: ssr: fix typo in doc comment

---
 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 f77f7c4fa8..3aabff824b 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:                                   *)
-- 
cgit v1.2.3


From d147b10a7fede25214416165b6a6ac10b6b827de Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Sun, 4 Mar 2018 18:14:21 +0100
Subject: ssr: add Prenex Implicits for Some_inj to use it as a view

---
 plugins/ssr/ssrfun.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index 3aabff824b..f44596cb7c 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -637,6 +637,9 @@ End Injections.
 
 Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed.
 
+(* Force implicits to use as a view. *)
+Prenex Implicits Some_inj.
+
 (* cancellation lemmas for dependent type casts.                             *)
 Lemma esymK T x y : cancel (@esym T x y) (@esym T y x).
 Proof. by case: y /. Qed.
-- 
cgit v1.2.3