From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 8 Sep 2010 16:31:02 +0000 (+0000)
Subject: better not allowed sort elimination error messsage
X-Git-Tag: make_still_working~2837
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=491d4b52a73ec28b4c8f28414d87d146e8caa40d;p=helm.git

better not allowed sort elimination error messsage
---

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