]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_ag/bagType.ml
the TypeError exception is back in place inside the Type modules
[helm.git] / helm / software / lambda-delta / basic_ag / bagType.ml
index c398e034dfeefb5c2e34328f4b575d63946b381d..02c831994775cf9bb43cbc7376098906eeeb1557 100644 (file)
@@ -19,6 +19,8 @@ module O = BagOutput
 module E = BagEnvironment
 module R = BagReduction
 
+exception TypeError of B.message
+
 (* Internal functions *******************************************************)
 
 let level = 4
@@ -29,13 +31,13 @@ let log1 s c t =
 
 let error1 st c t =
    let sc = "In the context" in
-   raise (R.TypeError (L.ct_items1 sc c st t))
+   raise (TypeError (L.ct_items1 sc c st t))
 
 let error3 c t1 t2 t3 =
    let sc, st1, st2, st3 = 
       "In the context", "the term", "is of type", "but must be of type"
    in
-   raise (R.TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3))
+   raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3))
 
 let mk_gref u l =
    let map t v = B.Appl (v, t) in