better error message

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index f9f3312408358fde025b1683cbfdebcd596d75e8..334ab86224bbd37b9d4b3345c1cb53696d8b6314 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -478,7 +478,7 @@ and strictly_positive ~subst context n nn te =
 (* the inductive type indexes are s.t. n < x <= nn *)
 and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
   match R.whd context te with
-  |  C.Appl ((C.Rel m)::tl) when m = i ->
+  |  C.Appl ((C.Rel m)::tl) as reduct when m = i ->
       let last =
        List.fold_left
         (fun k x ->
@@ -486,9 +486,10 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
           else
            match R.whd context x with
            |  C.Rel m when m = n - (indparamsno - k) -> k - 1
-           | _ -> raise (TypeCheckerFailure (lazy 
-              ("Non-positive occurence in mutual inductive definition(s) [1]" ^
-              NUri.string_of_uri uri))))
+           | y -> raise (TypeCheckerFailure (lazy 
+              ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
+              string_of_int indparamsno ^ " fixed) is not homogeneous in "^
+              "appl:\n"^ NCicPp.ppterm ~context ~subst ~metasenv:[] reduct))))
         indparamsno tl
       in
        if last = 0 then