Commit 2020-07-14 11:42 a0846da1View on Github →
chore(category_theory/limits/over): split a slow file (#3399)
This was previously the last file to finish compiling when compiling
category_theory/. This PR splits it into some smaller pieces which can compile in parallel (and some pieces now come earlier in the import hierarchy).
No change to content.
deleted def category_theory.over.over_has_terminal
added def category_theory.over.over_has_terminal