- instantiate rdb test_eq_only metasenv subst context m lc'
- (NCicReduction.head_beta_reduce ~subst t1) (not swap)
+ instantiate status test_eq_only metasenv subst context m lc'
+ (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
+ | C.Meta (n,lc), C.Meta (m,lc') when
+ let _,_,tyn = NCicUtils.lookup_meta n metasenv in
+ let _,_,tym = NCicUtils.lookup_meta m metasenv in
+ let tyn = NCicSubstitution.subst_meta status lc tyn in
+ 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
+ | _,_ -> false ->
+ instantiate status test_eq_only metasenv subst context m lc'
+ (NCicReduction.head_beta_reduce status ~subst t1) (not swap)