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/ssr') 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: *) -- 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 +++ test-suite/bugs/closed/6910.v | 5 +++++ 2 files changed, 8 insertions(+) create mode 100644 test-suite/bugs/closed/6910.v (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. diff --git a/test-suite/bugs/closed/6910.v b/test-suite/bugs/closed/6910.v new file mode 100644 index 000000000..5167a5364 --- /dev/null +++ b/test-suite/bugs/closed/6910.v @@ -0,0 +1,5 @@ +From Coq Require Import ssreflect ssrfun. + +(* We should be able to use Some_inj as a view: *) +Lemma foo (x y : nat) : Some x = Some y -> x = y. +Proof. by move/Some_inj. Qed. -- cgit v1.2.3