From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 8 Apr 2008 14:54:14 +0000 (+0000)
Subject: j off by one in error message
X-Git-Tag: make_still_working~5407
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=810bbac9ad50436ada9f2f5a9b069b3f59e079ab;p=helm.git

j off by one in error message
---

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