X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=57bafe0a38d9af871ee5a4769a58fbf99e3b2c1a;hb=86b0a224bd9251ed22648de04bc0d00f11dbd0fc;hp=d45b14fc9f3a1cfb14b0377e5d2f3ac96250d7b0;hpb=e499c2e36d8a39c4749b8e0e34438b49532d15b8;p=helm.git

diff --git a/matitaB/components/ng_refiner/nCicUnification.ml b/matitaB/components/ng_refiner/nCicUnification.ml
index d45b14fc9..57bafe0a3 100644
--- a/matitaB/components/ng_refiner/nCicUnification.ml
+++ b/matitaB/components/ng_refiner/nCicUnification.ml
@@ -590,7 +590,7 @@ and fo_unif0 during_delift status swap test_eq_only metasenv subst context (norm
       let tym = NCicSubstitution.subst_meta status lc tym in
        match tyn,tym with
           NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
-           NCicEnvironment.universe_lt u1 u2
+           NCicEnvironment.universe_lt status u1 u2
         | _,_ -> false ->
       instantiate status test_eq_only metasenv subst context m lc'
         (NCicReduction.head_beta_reduce status ~subst t1) (not swap)