X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;fp=matitaB%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=4f8be9c53583755ea6332df49d685f3de6e041a0;hb=86b0a224bd9251ed22648de04bc0d00f11dbd0fc;hp=7cdeb875e19d585baad9e65c3df1482f5cae410d;hpb=e499c2e36d8a39c4749b8e0e34438b49532d15b8;p=helm.git

diff --git a/matitaB/components/ng_refiner/nCicRefiner.ml b/matitaB/components/ng_refiner/nCicRefiner.ml
index 7cdeb875e..4f8be9c53 100644
--- a/matitaB/components/ng_refiner/nCicRefiner.ml
+++ b/matitaB/components/ng_refiner/nCicRefiner.ml
@@ -506,6 +506,11 @@ and try_coercions status
   (* we try with a coercion *)
   let rec first exc = function
   | [] ->   
+     let expty =
+      match expty with
+         `Type expty -> status#ppterm ~metasenv ~subst ~context expty
+       | `Sort -> "[[sort]]"
+       | `Prod -> "[[prod]]" in
       pp (lazy "WWW: no more coercions!");      
       raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
         "The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
@@ -886,7 +891,7 @@ and try_coercions status
       `Type expty -> expty
     | `Sort ->
         NCic.Sort (NCic.Type 
-         (match NCicEnvironment.get_universes () with
+         (match NCicEnvironment.get_universes status with
            | x::_ -> x 
            | _ -> assert false))
     | `Prod -> NCic.Prod ("_",NCic.Implicit `Type,NCic.Implicit `Type)
@@ -1260,7 +1265,7 @@ let typeof_obj
                 NCicReduction.whd status ~subst [] ty_sort
                with
                   (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
-                   if not (NCicEnvironment.universe_leq u1 u2) then
+                   if not (NCicEnvironment.universe_leq status u1 u2) then
                     raise
                      (RefineFailure
                        (lazy(localise te, "The type " ^