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 +-
 kernel/univ.ml        | 2 +-
 kernel/vars.ml        | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel')

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 ->
diff --git a/kernel/univ.ml b/kernel/univ.ml
index cb09e2d6d0..88b4e650f1 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -238,7 +238,7 @@ module Hashconsing = struct
 	| Nil -> l
 	| Cons (a, aa) -> 
 	  let a' = f a in 
-	    if a' == f a then
+	    if a' == a then
 	      let aa' = loop aa in
 		if aa' == aa then l
 		else cons a aa'
diff --git a/kernel/vars.ml b/kernel/vars.ml
index a9f4644abf..40a797a902 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -295,7 +295,7 @@ let subst_univs_level_constr subst c =
 	   if u' == u then t else 
 	     (changed := true; mkSort (Sorts.sort_of_univ u'))
       | _ -> Constr.map aux t
-    in 
+    in
     let c' = aux c in
       if !changed then c' else c
 
-- 
cgit v1.2.3