From d147b10a7fede25214416165b6a6ac10b6b827de Mon Sep 17 00:00:00 2001
From: Anton Trunov <anton.a.trunov@gmail.com>
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/ssr')

diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index 3aabff824..f44596cb7 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