sort CProp added

[helm.git] / helm / ocaml / cic_omdoc / doubleTypeInference.ml

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index 03227ef9b75df7af38c9bcac6db2f8e9d201d737..f51c00c74dc3271d861a2d7ab0b9a65313b75baf 100644 (file)
--- 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!!! *)
     | (_,_) ->