sort_of_prod relaxed to accept also Metas (when the second Meta has an

empty context). In this case the second Meta is returned.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index b6b40f3d1135727f40b475641861ded329df73f9..3959795055c0d8b9a2be4a9009c0f588b4419de5 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1637,6 +1637,9 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
         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 (_,[]))
+    | (C.Sort _, C.Meta (_,[])) -> t2'
     | (_,_) -> raise (TypeCheckerFailure (sprintf
         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
           (CicPp.ppterm t2')))