- Fix eq_constr_universes restricted to Sorts.equal

- Fix passing of universe contexts through definitions/proofs, abstract is ok now, even
  in presence of polymorphism
- Correctly mark unresolvable the evars made by the Simple abstraction.

2 files changed, 3 insertions, 5 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 4f2935be51..13e1abacc1 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -471,7 +471,7 @@ let compare_head_gen eq_universes eq_sorts f t1 t2 =
   | Rel n1, Rel n2 -> Int.equal n1 n2
   | Meta m1, Meta m2 -> Int.equal m1 m2
   | Var id1, Var id2 -> Id.equal id1 id2
-  | Sort s1, Sort s2 -> Sorts.equal s1 s2
+  | Sort s1, Sort s2 -> eq_sorts s1 s2
   | Cast (c1,_,_), _ -> f c1 t2
   | _, Cast (c2,_,_) -> f t1 c2
   | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 0959fa7033..8c4ec8cbfc 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -146,7 +146,7 @@ let infer_declaration env kn dcl =
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let (body, ctx), side_eff = Future.join body in
-      let env = push_context_set ctx env in
+      assert(Univ.ContextSet.is_empty ctx);
       let body = handle_side_effects env body side_eff in
       let def, typ, proj = 
 	match c.const_entry_proj with
@@ -172,9 +172,7 @@ let infer_declaration env kn dcl =
 	  let def = Def (Mod_subst.from_val j.uj_val) in
 	    def, typ, None
       in
-      let univs = Univ.UContext.union c.const_entry_universes 
-	(Univ.ContextSet.to_context ctx)
-      in
+      let univs = c.const_entry_universes in
 	feedback_completion_typecheck feedback_id;
 	def, typ, proj, c.const_entry_polymorphic,
         univs, c.const_entry_inline_code, c.const_entry_secctx