From 9c2f11b475fe7a62a3e7213efeacba2378cdfc96 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Apr 2008 14:47:15 +0000 Subject: [PATCH] better error message --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) 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 -- 2.39.2