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 ^ "=<=" ^
metasenv, subst
| (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
- C.Match (ref2,outtype2,term2,pl2)) ->
+ C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
let _,_,ty,_ = List.nth itl tyno in
let rec remove_prods ~subst context ty =
| C.Sort C.Prop -> true
| _ -> false
in
- if not (Ref.eq ref1 ref2) then
+ (* if not (Ref.eq ref1 ref2) then
raise (Uncertain (mk_msg metasenv subst context t1 t2))
- else
+ else*)
let metasenv, subst =
unify rdb test_eq_only metasenv subst context outtype1 outtype2 swap in
let metasenv, subst =