- double_type_of: sort_of_prod modified to expect also a meta

[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 3163dfe09bf21804932f3a4cabefad32745e1752..3c6f4129ac805a0d2b8075b9b9db83d831b33992 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -672,6 +672,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         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!!! *)
+    | (C.Meta _, C.Sort _) -> t2'
+    | (C.Meta _, (C.Meta (_,_) as t))
+    | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
+        t2'
     | (_,_) ->
       raise
        (NotWellTyped