Find a consistent way to deal with private lemmas
See the following discussion in !986 (merged).
We want a proper way to deal with "private lemmas" so that:
- They do not pollute the namespace when importing the module
- They are not found by
Search
Local Lemma
solves the first, but not the latter. There are hacks such as adding Private_
to the name to blacklist them from search, but they are ugly. They are also inconsistent with the _
proposal for "private" Ltacs from #529.