diff options
| author | Anton Trunov | 2018-03-21 15:47:58 +0100 |
|---|---|---|
| committer | Anton Trunov | 2018-03-21 23:09:56 +0100 |
| commit | c6139d34289b95b0f5ea30133daaf7c4cb13a49d (patch) | |
| tree | 550d3df7837b8b2ee9ffdc03a4d4e6c4283f2d60 /mathcomp | |
| parent | ae8e96a37644a4d1cded1b13acf031d1325b68b4 (diff) | |
Declare prenex implicits for `Some_inj`
This backports the changes from Coq's [PR #6911](https://github.com/coq/coq/pull/6911)
And also fixes a typo in doc comments
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrfun.v | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.6/ssrfun.v | 5 |
2 files changed, 8 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrfun.v b/mathcomp/ssreflect/plugin/v8.5/ssrfun.v index 48cf417..c517b92 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssrfun.v +++ b/mathcomp/ssreflect/plugin/v8.5/ssrfun.v @@ -181,7 +181,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: *) @@ -732,6 +732,9 @@ End Injections. Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed. +(* Forcing implicit arguments to be added when used 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/mathcomp/ssreflect/plugin/v8.6/ssrfun.v b/mathcomp/ssreflect/plugin/v8.6/ssrfun.v index 48cf417..c517b92 100644 --- a/mathcomp/ssreflect/plugin/v8.6/ssrfun.v +++ b/mathcomp/ssreflect/plugin/v8.6/ssrfun.v @@ -181,7 +181,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: *) @@ -732,6 +732,9 @@ End Injections. Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed. +(* Forcing implicit arguments to be added when used 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. |