Global Set Primitive Projections

This is on top of #638.

```
Idempotents got waay faster, though Factorization got somewhat slower.
Not quite sure what's up with that.

After    | File Name                                                 | Before   || Change
--------------------------------------------------------------------------------------------
3m47.71s | Total                                                     | 4m20.05s || -0m32.33s
--------------------------------------------------------------------------------------------
0m01.88s | Idempotents                                               | 0m30.73s || -0m28.85s
0m16.40s | Factorization                                             | 0m05.88s || +0m10.51s
0m17.75s | hit/V                                                     | 0m21.02s || -0m03.26s
0m02.78s | Modalities/Modality                                       | 0m06.33s || -0m03.55s
0m50.97s | categories/Adjoint/Pointwise                              | 0m53.29s || -0m02.32s
0m02.58s | Basics/Equivalences                                       | 0m00.66s || +0m01.92s
0m01.71s | categories/ExponentialLaws/Law1/Law                       | 0m02.71s || -0m01.00s
```

@mattam82, do you have any updates on [bug 3709](https://coq.inria.fr/bugs/show_bug.cgi?id=3709) and [bug 3782](https://coq.inria.fr/bugs/show_bug.cgi?id=3782)?  Should we wait for these to be fixed, or merge this as-is?