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/Make | |
| 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/Make')
0 files changed, 0 insertions, 0 deletions