HoTT/HoTT — pull request #577 by mikeshulman (2014-10-16 23:34:04+00:00)
Title: Use _ind and _rec for eliminators, close #517

As proposed at #517, this uses `_ind` for the dependent eliminator and `_rec` for the nondependent one across the board. There was a slight snag in implementing this for ordinary (non-higher) inductive types, because Coq's `induction` tactic appears to hardcode the suffixes `_rect`, `_rec`, and `_ind`. So rather than making `_rect` a parsing notation for `_ind`, I made it a `Definition` for it, at least in the cases of inductive types defined by us. In the case of inductive types defined in the coq stdlib file `Datatypes.v`, I left the definition of `_rect` there since (at least in some cases) it gets used by `induction` elsewhere in the stdlib, and then redefined the `_ind` version in our files.

Moreover, in the case of `nat` I had to leave Coq's version of `_rec` (meaning the dependent eliminator into `Set`) in `Datatypes.v`, since Coq's `nat` lands in `Set` and `induction` wants to use `_rec` when the target is in `Set`. Then I created `Types/Nat.v` to hold a definition of `nat_ind` for us. This raises another question, though: do we want to use the `nat` from the stdlib, and if so, should we modify the stdlib so that it doesn't land in `Set`? Or should we define our own type `Nat` in `Types/Nat.v` the way we did for `Bool`?