(lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^
"has type %s\nnot convertible with %s")
(NCicPp.ppterm ~subst ~metasenv ~context
- (C.Const (Ref.mk_constructor j r)))
- (NCicPp.ppterm ~metasenv ~subst ~context (List.nth pl (j-1)))
+ (C.Const (Ref.mk_constructor (j-1) r)))
+ (NCicPp.ppterm ~metasenv ~subst ~context (List.nth pl (j-2)))
(NCicPp.ppterm ~metasenv ~subst ~context p_ty)
(NCicPp.ppterm ~metasenv ~subst ~context exp_p_ty))));
let res = outtype::arguments@[term] in