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

5 files changed, 26 insertions, 16 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 ->
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
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 02e671a5c1..37064b0a7c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -50,10 +50,6 @@ let evars_to_goals p evm =
 
 open Auto
 
-let e_give_exact flags (c,cl) gl =
-  let t1 = (pf_type_of gl c) in
-    tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
-
 open Unification
 
 let auto_unif_flags = {
@@ -91,6 +87,19 @@ let progress_evars t =
     in t <*> check
   end
 
+
+let e_give_exact flags poly (c,clenv) gl =
+  let c, gl =
+    if poly then
+      let clenv', subst = Clenv.refresh_undefined_univs clenv in
+      let clenv' = connect_clenv gl clenv' in
+      let c = Vars.subst_univs_level_constr subst c in
+	c, {gl with sigma = clenv'.evd}
+    else c, gl
+  in
+  let t1 = pf_type_of gl c in
+    tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
+
 let unify_e_resolve poly flags (c,clenv) gls =
   let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
   let clenv' = connect_clenv gls clenv' in
@@ -103,8 +112,8 @@ let unify_resolve poly flags (c,clenv) gls =
   let clenv' = clenv_unique_resolver ~flags clenv' gls in
     Clenvtac.clenv_refine false(*uhoh, was true*) ~with_classes:false clenv' gls
 
-let clenv_of_prods nprods (c, clenv) gls =
-  if Int.equal nprods 0 then Some clenv
+let clenv_of_prods poly nprods (c, clenv) gls =
+  if poly || Int.equal nprods 0 then Some clenv
   else
     let ty = pf_type_of gls c in
     let diff = nb_prod ty - nprods in
@@ -113,8 +122,8 @@ let clenv_of_prods nprods (c, clenv) gls =
 	Some (mk_clenv_from_n gls (Some diff) (c,ty))
       else None
 
-let with_prods nprods (c, clenv) f gls =
-  match clenv_of_prods nprods (c, clenv) gls with
+let with_prods nprods poly (c, clenv) f gls =
+  match clenv_of_prods poly nprods (c, clenv) gls with
   | None -> tclFAIL 0 (str"Not enough premisses") gls
   | Some clenv' -> f (c, clenv') gls
 
@@ -158,11 +167,11 @@ and e_my_find_search db_list local_db hdc complete concl =
     fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
       let tac =
 	match t with
-	  | Res_pf (term,cl) -> with_prods nprods (term,cl) (unify_resolve poly flags)
-	  | ERes_pf (term,cl) -> with_prods nprods (term,cl) (unify_e_resolve poly flags)
-	  | Give_exact c -> e_give_exact flags c
+	  | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags)
+	  | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags)
+	  | Give_exact c -> e_give_exact flags poly c
 	  | Res_pf_THEN_trivial_fail (term,cl) ->
-              tclTHEN (with_prods nprods (term,cl) (unify_e_resolve poly flags))
+              tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
 	        (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])
 	  | Extern tacast ->
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 45dd6f1ec1..2b00a6d867 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -172,9 +172,10 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	  [] subst (snd k.cl_context)
 	in
 	let (_, ty_constr) = instance_constructor (k,u) subst in
+	let nf, subst = Evarutil.e_nf_evars_and_universes evars in
 	let termtype =
 	  let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-	    fst (Evarutil.e_nf_evars_and_universes evars) t
+	    nf t
 	in
 	Evarutil.check_evars env Evd.empty !evars termtype;
 	let ctx = Evd.universe_context !evars in