]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_ag/bagReduction.ml
the TypeError exception is back in place inside the Type modules
[helm.git] / helm / software / lambda-delta / basic_ag / bagReduction.ml
index 4e147ae6d247f5fb6b34faddd07ab598098a8e9b..c2de019cd57628f8e250a239509d541340910ae8 100644 (file)
@@ -17,8 +17,6 @@ module O = BagOutput
 module E = BagEnvironment
 module S = BagSubstitution
 
-exception TypeError of B.message
-
 type machine = {
    i: int;
    c: B.context;
@@ -45,17 +43,13 @@ let term_of_whdr = function
 
 let level = 5
 
-let error i = 
-   let s = Printf.sprintf "local reference not found %u" i in
-   raise (TypeError (L.items1 s))
-
 let log1 s c t =
    let sc, st = s ^ " in the context", "the term" in
    L.log O.specs level (L.ct_items1 sc c st t)
 
 let log2 s cu u ct t =
    let s1, s2, s3 = s ^ " in the context", "the term", "and in the context" in
-   L.log O.specs level (L.ct_items2 s1 cu s2 u s3 ct s2 t)
+   L.log O.specs level (L.ct_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
 
 let empty_machine = {i = 0; c = B.empty_context; s = []}
 
@@ -73,7 +67,7 @@ let unwind_stack f m =
 let get f c m i =
    let f = function
       | Some (_, b) -> f b
-      | None        -> error i
+      | None        -> assert false
    in
    let f c = B.get f c i in
    B.append f c m.c