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 b9a585f97e0eeaa10d776e166d97c4392afc4ff2..287cf8cd965d1b6ac0f80466a421427f631ad771 100644 (file)
--- 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