From 810bbac9ad50436ada9f2f5a9b069b3f59e079ab Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 14:54:14 +0000 Subject: [PATCH] j off by one in error message --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index b9a585f97..287cf8cd9 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -750,8 +750,8 @@ let rec typeof ~subst ~metasenv context term = (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 -- 2.39.2