HoTT/HoTT — pull request #640 by JasonGross (2014-12-12 08:54:14+00:00)
Title: 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?