From 1dd78acac418c0f69abb8d9f5d8db13351f01ccc Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 22 Nov 2013 12:35:33 +0100
Subject: 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
---
 kernel/term_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term_typing.ml')

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 ->
-- 
cgit v1.2.3