X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftacticals.ml;fp=helm%2Focaml%2Ftactics%2Ftacticals.ml;h=62f1ce322c4a98be3b42ef890700b6588e903de5;hb=90c15accf8c385a3dc44aa5f6df13f707514e2cd;hp=4e0e04914bd1ac9bcafa04f8c9d1c1c4cff14308;hpb=98c386d8d12a2fe4d64017e0b1bf684b22fe6423;p=helm.git

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 4e0e04914..62f1ce322 100644
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -94,7 +94,12 @@ let thens ~start ~continuations =
        (proof',goals@new_goals')
     ) (proof,[]) new_goals continuations
   with
-   Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
+   Invalid_argument _ -> 
+(* FG: more debugging information *)
+    let debug = Printf.sprintf "thens: expected %i new goals, found %i"
+     (List.length continuations) (List.length new_goals)
+    in
+    raise (Fail debug)
  in
   mk_tactic (thens ~start ~continuations )