From fbe2b073c8a78abd5e8c65eff92158357997e370 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 5 Feb 2004 16:43:15 +0000 Subject: [PATCH] sort_of_prod relaxed to accept also Metas (when the second Meta has an empty context). In this case the second Meta is returned. --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index b6b40f3d1..395979505 100644 --- 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'))) -- 2.39.2