This commit patches the environment and the library so that their status is

[helm.git] / matitaB / components / ng_refiner / nCicRefiner.ml

diff --git a/matitaB/components/ng_refiner/nCicRefiner.ml b/matitaB/components/ng_refiner/nCicRefiner.ml
index 4645e6f6eb55d14d68c96b08808c37510bdd78ff..8deb72797c5d690b0de62f48f4476584c4828938 100644 (file)
--- 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 " ^