From 3cc0493b8b8b6eba59655855e4e5dadd335563c0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 3 Feb 2016 11:38:58 +0100
Subject: resolve type classes under the correct set of univs (fix #22)

---
 mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'mathcomp/ssreflect/plugin/trunk')

diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
index dbc7f8b..864db5b 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
@@ -346,6 +346,7 @@ let unif_end env sigma0 ise0 pt ok =
   let ise = Evarconv.consider_remaining_unif_problems env ise0 in
   let s, uc, t = nf_open_term sigma0 ise pt in
   let ise1 = create_evar_defs s in
+  let ise1 = Evd.set_universe_context ise1 uc in
   let ise2 = Typeclasses.resolve_typeclasses ~fail:true env ise1 in
   if not (ok ise) then raise NoProgress else
   if ise2 == ise1 then (s, uc, t)
-- 
cgit v1.2.3