(no commit message)

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

diff --git a/matitaB/components/ng_refiner/nCicUnification.ml b/matitaB/components/ng_refiner/nCicUnification.ml
index d45b14fc9f3a1cfb14b0377e5d2f3ac96250d7b0..57bafe0a38d9af871ee5a4769a58fbf99e3b2c1a 100644 (file)
--- 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)