Final polish concerning #543

Note:
```coq
Scheme Minimality for Empty Sort Type.
Print Empty_rect_nodep. (*
Empty_rect_nodep =
fun (P : Type) (e : Empty) => match e return P with
                              end
     : forall P : Type, Empty -> P *)
```
We can even do
```coq
Unset Elimination Schemes.
Inductive Empty : Type1 := .
Set Elimination Schemes.
Scheme Empty_rec := Minimality for Empty Sort Type.
Scheme Empty_rect := Induction for Empty Sort Type.
```
Do we want to use this?