sort CProp added

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 881c72bfd516852218105dc56ce71653219ce4d8..ba79ce92232f4cce5866786b6d6b8ea4e4b3133e 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -290,7 +290,7 @@ and type_of_aux' metasenv context t =
     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,subst',metasenv'
      | (C.Sort s1, C.Sort s2) ->
          (*CSC manca la gestione degli universi!!! *)