X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=fcc76b0adc5bf72b38129bd36a3ddca7952d4676;hb=8a218c35f9bde765a73f14867a294c874f9dc15c;hp=e2f6a7090ded821e685a5bb6ce3c8be1ed3293e2;hpb=9078eadc955930e7e37cfc2451a40416512c95fa;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index e2f6a7090..fcc76b0ad 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -382,8 +382,8 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
        | _ ->
         let lty = NCicSubstitution.subst_meta lc ty in
         pp (lazy ("On the types: " ^
-          ppterm ~metasenv ~subst ~context lty ^ "=<=" ^
-          ppterm ~metasenv ~subst ~context ty_t)); 
+          ppterm ~metasenv ~subst ~context ty_t ^ "=<=" ^
+          ppterm ~metasenv ~subst ~context lty)); 
         let metasenv, subst = 
           unify rdb false metasenv subst context ty_t lty false
         in
@@ -559,6 +559,17 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
               len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
           instantiate rdb test_eq_only metasenv subst context m lc'
             (NCicReduction.head_beta_reduce ~subst t1) (not swap)
+       | C.Meta (n,lc), C.Meta (m,lc') when
+          let _,_,tyn = NCicUtils.lookup_meta n metasenv in
+          let _,_,tym = NCicUtils.lookup_meta m metasenv in
+          let tyn = NCicSubstitution.subst_meta lc tyn in
+          let tym = NCicSubstitution.subst_meta lc tym in
+           match tyn,tym with
+              NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
+               NCicEnvironment.universe_lt u1 u2
+            | _,_ -> false ->
+          instantiate rdb test_eq_only metasenv subst context m lc'
+            (NCicReduction.head_beta_reduce ~subst t1) (not swap)
        | C.Meta (n,lc), t -> 
           instantiate rdb test_eq_only metasenv subst context n lc 
             (NCicReduction.head_beta_reduce ~subst t) swap
@@ -865,7 +876,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
          | KeepReducing _ -> assert false
          | KeepReducingThis _ ->
             assert (not (norm1 && norm2));
-	    unif_machines metasenv subst (small_delta_step ~subst m1 m2)
+            unif_machines metasenv subst (small_delta_step ~subst m1 m2)
          | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
            -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
          | UnificationFailure msg