The tactic interpreter now uses a new type of tactics, through
the GTac module. A ['a Gtac.t] is a special case of tactic that
may depend on the current goals, or not. Internally, it construct
a list of results, one for each focussed goal, if the tactic is
actually dependent.

This allows for an interpretation of whole-goal tactic that does
work, which was not the case for the previous implementation,
which did to many Proofview.Goal.enter.
A bug has been closed (HoTT/coq #105)
cbn understand ! Arguments directive

Of course, this is an under approximation of the expected behavior : unfolding
a constant iff a leaf of its underlying split-tree is reached.
- Keep all <= constraints during refinement, otherwise we might miss collapsed universes.
- Fix normalization with universe substitutions during refinement being inconsistent
with the one in the kernel.
Fix handling of anonymous Type in template universe polymorphic inductives
to not interfere with already declared universes.
- Fix hashing of levels to get the "right" order in universe contexts etc...
- Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}.
These are always rigid.
- Use level-to-level substitutions where the more general level-to-universe substitutions
were previously used.
- Force every universe level to be >= Prop, so one cannot "go under" it anymore.
- Finish the change to level-to-level substitutions, in the checker.
- Allow parsing of @const@{instance} for specifying universe instances of polymorphic
constants.
Fix canonical structure resolution (makes test-suite files go through again).
- Better parsing and printing of named universes: Type{ident} and foo@{(ident|Prop|Set|Type|' ')*}
(user given names are still write only).
- Add test-suite file for named universes.
Remove spurious Show in script.