Merge branch 'robbert/small_mrs' into 'master'

Expand `CONTRIBUTING.md` with information that we prefer small merge requests.

See merge request iris/iris!723

CONTRIBUTING.md

@@ -36,6 +36,12 @@ a feature branch instead.
 [jung]: https://gitlab.mpi-sws.org/jung
 [iris]: https://gitlab.mpi-sws.org/iris/iris
 
+We prefer small and self-contained merge requests that add a single feature
+over merge requests that add arbitrary collections of lemmas. Small merge
+requests are easier to review, and will typically be merged more quickly
+(because it avoids blocking the whole merge request on a single
+discussion).
+
 ## How to update the std++ dependency
 
 * Do the change in std++, push it.