HoTT coq bug #62 fixed.
- Fix bug in unification, not only named metas are turned into evars (e.g. in Ssreflect).
- Fix is_applied_rewrite_relation to look for propositional relations.
Adding a raw_goals primitive for Tacinterp.
Add an e_type_of to avoid losing universe constraints.
Cleanup treatment of template universe polymorphism (thanks to E. Tassi
for helping fixing this).

Now the issue is handled solely through refreshing of the terms assigned
to evars during unification.
If ?X = list ?Y, then Y's type is refreshed so that it doesn't mention
a template universe and in turn, ?X won't. Same goes when typechecking
(nil ?X, nil ?Y), the pair constructor levels will be set higher than fresh
universes for the lists carriers. This also handles user-defined functions
on template polymorphic inductives, which was fragile before.
Pretyping and Evd are now uncluttered from template-specific code.
Bug 27 closed now that universe contexts can be refined during the proof,
here instantiating a flexible level with Set.