- j,false
- ) (1,true) pl
- in
- if not branches_ok then
- raise
- (TypeCheckerFailure
- (lazy (Printf.sprintf "Branch for constructor %s has wrong type"
- (NCicPp.ppterm (C.Const
- (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j))))))));
- let res = outtype::arguments@[term] in
- R.head_beta_reduce (C.Appl res)
+ j,false,old_p_ty,old_exp_p_ty
+ ) (1,true,C.Sort C.Prop,C.Sort C.Prop) pl
+ in
+ if not branches_ok then
+ raise
+ (TypeCheckerFailure
+ (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^
+ "has type %s\nnot convertible with %s") (NCicPp.ppterm (C.Const
+ (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)))))
+ (NCicPp.ppterm ~context (List.nth pl (j-1)))
+ (NCicPp.ppterm ~context p_ty) (NCicPp.ppterm ~context exp_p_ty))));
+ let res = outtype::arguments@[term] in
+ R.head_beta_reduce (C.Appl res)