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=8deb72797c5d690b0de62f48f4476584c4828938;hb=e79c8b830f9f6b0c3f4d577909e32e1bb4032cdf;hp=4645e6f6eb55d14d68c96b08808c37510bdd78ff;hpb=9dac2c325dca1b5b92d6ba11dadf470538bae28e;p=helm.git

diff --git a/matitaB/components/ng_refiner/nCicRefiner.ml b/matitaB/components/ng_refiner/nCicRefiner.ml
index 4645e6f6e..8deb72797 100644
--- a/matitaB/components/ng_refiner/nCicRefiner.ml
+++ b/matitaB/components/ng_refiner/nCicRefiner.ml
@@ -189,7 +189,7 @@ let rec typeof (status:#NCicCoercion.status)
         in
         metasenv, subst, t, infty
     | C.Sort s -> 
-         (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort s)
+         (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort status s)
          with 
          | NCicEnvironment.UntypableSort msg -> 
               raise (RefineFailure (lazy (localise t, Lazy.force msg)))
@@ -855,7 +855,7 @@ and force_to_sort status metasenv subst context t orig_t localise ty =
         let ty = NCicReduction.whd status ~subst context ty in
           try_coercions status ~localise metasenv subst context
             t orig_t ty (NCic.Sort (NCic.Type 
-              (match NCicEnvironment.get_universes () with
+              (match NCicEnvironment.get_universes status with
                | x::_ -> x 
                | _ -> assert false))) false 
              (Uncertain (lazy (localise orig_t, 
@@ -1204,7 +1204,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 " ^