fix(kernel/metavar): avoid crash due to stack overflow, closes #253
feat(kernel/inductive): add API for retrieving the number of indices in an inductive datatype
feat(kernel/inductive): expose 'get_elim_name' API
feat(kernel/inductive): add get_num_minor_premises and get_num_type_formers APIs
feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes
feat(library/definitional/induction_on): automatically add 'induction_on'
refactor(library/data/unit): make unit universe polymorphic

Motivation: we need it for "padding".
Example 1: defining a n-ary tuple type.
Example 2: defining cases-on for mutually recursive datatypes
feat(library/hott) add adjointification proof up to two gaps
fix(library/hott) close gaps and clean up adjointification proof
feat(library/hott) add the proof that the inverse of an equivalence is an equivalence

This is done by changing the order of theorems and using the adjointification.
refactor(library/data/unit): break unit.lean into smaller pieces

The unit datatype is used by automation.

We want to be able to access its declaration without having to access
all dependencies (e.g., decidable, subsingleton, inhabited, ...).

This is *not* an optimization, but a way to make sure we can "import" unit
before we import other declarations.
fix(library/definitional): make sure argument is an inductive datatype
chore(library/definitional): remove dead code
feat(library/definitional/cases_on): automatically add 'cases_on'
fix(frontends/lean/inductive_cmd): include 'induction_on', 'cases_on', and 'rec_on' into .ilean index file
fix(library/data/unit): missing file
fix(emacs/lean-syntax): syntax highlight for composite names in declarations
fix(frontends/lean/parser): add two kinds of no_undef_id behavior: to (global) constant; to local constant
fix(frontends/lean/parser): save identifier info for undef local
feat(library/tactic/exact_tactic): modify 'exact' tactic semantics, use higher-order unification

See new node.inj4 theorem, we need the extra power to be able to avoid type information at
    exact (assume e₁ e₂, e₁)