Various fixes of universe polymorphism and projections when they're set.

- Fix substitution of universes!
- Properly refresh universes in typeclasses exact hints.

Conflicts:
	kernel/term_typing.ml
	toplevel/obligations.ml

1 files changed, 1 insertions, 1 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index dc2ddea4a3..7c5b8c7283 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -138,7 +138,7 @@ let infer_declaration env kn dcl =
 	    (* TODO: recognize projection *)
 	  let context, m = decompose_lam_n_assum (n + 1) body in 
 	  let body = it_mkLambda_or_LetIn body' context in
-	      (* let tj = infer_type env' (Option.get c.const_entry_type) in *)
+
 	    Def (Mod_subst.from_val (hcons_constr body)),
 	    RegularArity (hcons_constr (Option.get typ)), Some pb
 	| None ->