diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-07 11:08:55 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-07 11:08:55 +0100 |
| commit | 719a10381a7738f82ef5d6abc3d19accf99ad4f0 (patch) | |
| tree | 9e97c63011aed737b96c1eacfcfa90a55f24f272 /plugins/ssr | |
| parent | a72d7eeba0ece3ebcc49232762a28b27ab108ded (diff) | |
| parent | d147b10a7fede25214416165b6a6ac10b6b827de (diff) | |
Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrfun.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 96b6ed295..ac2c78249 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -165,7 +165,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: *) @@ -639,6 +639,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. |