X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=e9aa59dce7094eac40af0f8373cdd7410ecfe570;hb=b2e89f8c6a89ad675718acdf35cdd0abfafaad5a;hp=97a559a1799a604bbbade078e6c1c51d4939ddab;hpb=0991fc5486c3158fc361e84cbba5aefa67893ba4;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 97a559a..e9aa59d 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -46,7 +46,7 @@ let first bound p var f =
    try
     f p i
    with Backtrack s ->
-prerr_endline ("!!BACKTRACK!! " ^ s);
+prerr_endline (">>>>>> BACKTRACK (reason: " ^ s ^") measure=$ ");
      List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ;
 prerr_endline("Now trying var="^string_of_var var^" i="^string_of_int i);
      aux (i+1)
@@ -158,7 +158,7 @@ let super_simplify ({div; ps; conv} as p) =
 let cast_to_ps =
  function
     #i_num_var as y -> (y : i_num_var)
-  | `Bottom | `Pacman -> raise (Backtrack "foo")
+  | `Bottom | `Pacman -> raise (Backtrack "BOT/PAC in ps")
   | t ->
     prerr_endline (print (t :> nf));
     assert false (* algorithm failed *)