let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
+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 c u t =
+ let sc, su, st = s ^ " in the context", "the term", "and the term" in
+ L.log O.specs level (L.ct_items2 sc c su u st t)
+
let empty_machine = {i = 0; c = B.empty_context; s = []}
let inc m = {m with i = succ m.i}
let ho_whd f c t =
let f r = L.unbox level; f r in
- L.box level; L.log O.specs level (L.ct_items1 "Now scanning" c t);
+ L.box level; log1 "Now scanning" c t;
ho_whd f c empty_machine t
let rec are_convertible f xl c m1 t1 m2 t2 =
let rec aux m1 r1 m2 r2 =
let u, t = term_of_whdr r1, term_of_whdr r2 in
- L.log O.specs level (L.ct_items2 "Now really converting" c u "and" c t);
+ log2 "Now really converting" c u t;
match r1, r2 with
| Sort_ h1, Sort_ h2 ->
if h1 = h2 then f xl else f None
let are_convertible f c u t =
let f b = L.unbox level; f b in
- L.box level;
- L.log O.specs level (L.ct_items2 "Now converting" c u "and" c t);
+ L.box level; log2 "Now converting" c u t;
are_convertible f (Some []) c empty_machine u empty_machine t