diff options
| author | Enrico Tassi | 2016-02-03 11:38:58 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2016-02-03 11:38:58 +0100 |
| commit | 3cc0493b8b8b6eba59655855e4e5dadd335563c0 (patch) | |
| tree | 8dd9c12d83f43ebd83a44339d1d34b3cc39ec52c /mathcomp | |
| parent | 1a7d47ba610dc1b9775ba1b838d5b2238ce7df26 (diff) | |
resolve type classes under the correct set of univs (fix #22)
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 | 1 |
2 files changed, 2 insertions, 0 deletions
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) diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 index 0187a12..b16753a 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 +++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 @@ -345,6 +345,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) |