From: Stefano Zacchiroli Date: Tue, 3 Feb 2004 14:09:32 +0000 (+0000) Subject: removed SortExpectedMetaFound special exception X-Git-Tag: V_0_2_3~93 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e4525d2a61f8bc9967d165d7bfd710037fb09d79;p=helm.git removed SortExpectedMetaFound special exception --- diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 19ee778f5..b6b40f3d1 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -30,7 +30,6 @@ open Printf exception AssertFailure of string;; exception TypeCheckerFailure of string;; -exception SortExpectedMetaFound of string;; (* TODO temp *) let fdebug = ref 0;; let debug t context = @@ -1638,10 +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!!! *) - | (_,_) -> raise (SortExpectedMetaFound (sprintf + | (_,_) -> raise (TypeCheckerFailure (sprintf "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1') (CicPp.ppterm t2'))) -(* raise (TypeCheckerFailure (sprintf *) and eat_prods context hetype = (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli index b267429d4..95ee658c7 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -26,7 +26,6 @@ (* These are the only exceptions that will be raised *) exception TypeCheckerFailure of string exception AssertFailure of string -exception SortExpectedMetaFound of string val typecheck : UriManager.uri -> unit