From 17a2d79ff87d6b1942772b516e4d633347419c2e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 07:30:14 +0000 Subject: [PATCH] Error message improved. --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 00a1b6120..65e87e55d 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -720,12 +720,13 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl = let context,te = split_prods ~subst tys leftno te in let con_sort = typeof ~subst ~metasenv context te in (match R.whd ~subst context con_sort, R.whd ~subst [] ty_sort with - C.Sort (C.Type u1), C.Sort (C.Type u2) -> + (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) -> if not (E.universe_leq u1 u2) then raise (TypeCheckerFailure - (lazy ("The type of the constructor is not included in " ^ - "the inductive type sort"))) + (lazy ("The type " ^ PP.ppterm ~metasenv ~subst ~context s1^ + " of the constructor is not included in the inductive" ^ + " type sort " ^ PP.ppterm ~metasenv ~subst ~context s2))) | C.Sort _, C.Sort C.Prop | C.Sort C.CProp, C.Sort C.CProp | C.Sort _, C.Sort C.Type _ -> () -- 2.39.2