if is_type attrs then
metasenv,subst,true
else
+ let _,cc,ty = NCicUtils.lookup_meta n metasenv in
+ let metasenv,subst,ty = sortfy exc metasenv subst cc ty in
let metasenv =
NCicUntrusted.replace_in_metasenv n
- (fun attrs,cc,ty -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
+ (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
metasenv
in
metasenv,subst,false
if is_type attrs then
metasenv,subst,true
else
+ let _,cc,_,ty = NCicUtils.lookup_subst n subst in
+ let metasenv,subst,ty = sortfy exc metasenv subst cc ty in
let subst =
NCicUntrusted.replace_in_subst n
- (fun attrs,cc,bo,ty->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
+ (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
subst
in
optimize_meta metasenv subst (NCicSubstitution.subst_meta lc bo))
| _ -> assert false)
| `IsType
| `IsTerm ->
- (match ty,t with
- NCic.Implicit (`Typeof _), _ ->
+ (match ty with
+ NCic.Implicit (`Typeof _) ->
let (metasenv, subst), ty_t =
try
NCicMetaSubst.delift
in
delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv
subst
- | _, _ ->
+ | _ ->
let lty = NCicSubstitution.subst_meta lc ty in
pp (lazy ("On the types: " ^
ppterm ~metasenv ~subst ~context lty ^ "=<=" ^
| NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
+ | C.Meta (n,_), C.Meta (m,lc') when
+ let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
+ let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
+ (n < m && cc1 = cc2) ||
+ let len1 = List.length cc1 in
+ let len2 = List.length cc2 in
+ len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
+ instantiate rdb test_eq_only metasenv subst context m lc'
+ (NCicReduction.head_beta_reduce ~subst t1) (not swap)
| C.Meta (n,lc), t ->
instantiate rdb test_eq_only metasenv subst context n lc
(NCicReduction.head_beta_reduce ~subst t) swap