Use full transparent state when checking well-typedness of a second order matching
infered predicate, instead of the arguments ts which might be empty (e.g. in unification).
Fixes failure in success/unification.v
Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_depends.
Also add a missing constraint when generating a fresh universe for a template polymorphic
inductive in that case.
Use the right transparent state when comparing _types_ of metas.
In exact check, use e_type_of to ensure that universe constraints necessary
to typecheck the term are not forgotten. (relieves tactic implementors from
calling e_type_of themselves, e.g. in congruence). Fixes a bug found in Containers.