Use _ind and _rec for eliminators, close #517
oops, add Types/Nat
global unset elimination schemes
actually, we want Local Unset Elimination Schemes
define Empty_rect
elimination schemes for sig
Local Unset Elimination Schemes in Overture, with documentation
update STYLE to conform to the Types/ reorganization
Merge pull request #578 from mikeshulman/stylereorg

update STYLE to conform to the Types/ reorganization
missing Local in Bool
comments about Coq bug 3745
Merge pull request #577 from mikeshulman/indrec

Use _ind and _rec for eliminators, close #517
Some lemmas about commutative squares.

I thought these would be used in more places, but I only found one.
Merge pull request #580 from mikeshulman/commsq

Some lemmas about commutative squares.
most of the stuff in Basics/Fibrations is subsumed by Types/Sigma
move NullHomotopy into its own file
Merge pull request #581 from mikeshulman/fibrations

most of the stuff in Basics/Fibrations is subsumed by Types/Sigma
Merge pull request #582 from mikeshulman/nullhomotopy

move NullHomotopy into its own file
use `open_constr` in `simpl rewrite`
`simpl rewrite` with `Arguments` solves the rewrite problems in Factorization