X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=fc9dc840d1bb5323ff9526ce57d561664b5999ac;hb=4d765cc85e3a1e84c80c348a1e67ea1eed984916;hp=8fa6963aab637b62bcb145dc72eec52d1597b247;hpb=910c252965fe17d6b5af92e4658e7d02bac82d58;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 8fa6963aa..fc9dc840d 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -386,7 +386,14 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                  t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
               with
                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
-        | C.Sort _ -> 
+        | C.Sort (C.CProp tno) -> 
+            let tno' = CicUniv.fresh() in 
+             (try
+               let ugraph1 = CicUniv.add_gt tno' tno ugraph in
+                 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+        | C.Sort (C.Prop|C.Set) -> 
             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
         | C.Implicit infos ->
            let metasenv',t' = exp_impl metasenv subst context infos in