X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2FdoubleTypeInference.ml;h=f51c00c74dc3271d861a2d7ab0b9a65313b75baf;hb=49b54c2de0c8d449638e469d1c95bfae01b0aadc;hp=03227ef9b75df7af38c9bcac6db2f8e9d201d737;hpb=c706b1cb2c7cbdd23a3281d35d3f0b10c3a684cf;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index 03227ef9b..f51c00c74 100644
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -647,7 +647,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
    let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
    match (t1', t2') with
       (C.Sort s1, C.Sort s2)
-        when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
+        when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
     | (_,_) ->