firs wrking (?) version of lapply

[helm.git] / helm / ocaml / tactics / tacticals.ml

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 4e0e04914bd1ac9bcafa04f8c9d1c1c4cff14308..62f1ce322c4a98be3b42ef890700b6588e903de5 100644 (file)
--- 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 )