let tym = NCicSubstitution.subst_meta status lc tym in
match tyn,tym with
NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
- NCicEnvironment.universe_lt u1 u2
+ NCicEnvironment.universe_lt status u1 u2
| _,_ -> false ->
instantiate status test_eq_only metasenv subst context m lc'
(NCicReduction.head_beta_reduce status ~subst t1) (not swap)