X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=956372d60294a621f2aa6941aea5a4cd51c02831;hb=0b15dfdee3357a626c77d30599e87a83ab34e471;hp=bde5d63e413978703bf8ef0d58a9908f478d1d34;hpb=aba6841906f09875a5800f58b24862444a1f4baf;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index bde5d63e4..956372d60 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1104,7 +1104,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
         | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) -> 
             let t' = CicUniv.fresh() in 
              (try
-              let ugraph1 = CicUniv.add_gt t' t1 ugraph in
+              let ugraph1 = CicUniv.add_ge t' t1 ugraph in
               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
                 C.Sort (C.Type t'),subst,metasenv,ugraph2
               with