From 491d4b52a73ec28b4c8f28414d87d146e8caa40d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 8 Sep 2010 16:31:02 +0000 Subject: [PATCH] better not allowed sort elimination error messsage --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 02eec0576..ccbebc271 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -659,7 +659,7 @@ and check_allowed_sort_elimination ~subst ~metasenv r = (PP.ppterm ~subst ~metasenv ~context so) ))); (match arity1, R.whd ~subst ((name,C.Decl so)::context) ta with - | C.Sort s1, C.Sort s2 -> + | C.Sort s1, (C.Sort s2 as arity2) -> (match NCicEnvironment.allowed_sort_elimination s1 s2 with | `Yes -> () | `UnitOnly -> @@ -680,7 +680,11 @@ and check_allowed_sort_elimination ~subst ~metasenv r = is_non_informative ~metasenv ~subst leftno constrty)) then raise (TypeCheckerFailure (lazy - ("Sort elimination not allowed")))) + ("Sort elimination not allowed: " ^ + NCicPp.ppterm ~metasenv ~subst ~context arity1 + ^ " towards "^ + NCicPp.ppterm ~metasenv ~subst ~context arity2 + )))) | _ -> ()) | _,_ -> () in -- 2.39.2