From: Stefano Zacchiroli <zack@upsilon.cc>
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