- Relax identification of metas in Ltac to not compare universes syntactically.
- add constr_eq_nounivs tactic to compare constrs without comparing universes.