From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 14 Apr 2008 14:47:15 +0000 (+0000)
Subject: better error message
X-Git-Tag: make_still_working~5341
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9c2f11b475fe7a62a3e7213efeacba2378cdfc96;p=helm.git

better error message
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index f9f331240..334ab8622 100644
--- 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