- (fun attrs,cc,ty -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
+ (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
+ let _,cc,_,ty = NCicUtils.lookup_subst n subst in
+ let metasenv,subst,ty = sortfy exc metasenv subst cc ty in
- (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)
let lty = NCicSubstitution.subst_meta lc ty in
pp (lazy ("On the types: " ^
ppterm ~metasenv ~subst ~context lty ^ "=<=" ^
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),
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 =
let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
let _,_,ty,_ = List.nth itl tyno in
let rec remove_prods ~subst context ty =