X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftacticals.ml;h=3c89150adb96f80b1e1721e433eccce810c0d3e4;hb=22964c949671af4b5e739b06b915a81a4fc2c5b5;hp=4e0e04914bd1ac9bcafa04f8c9d1c1c4cff14308;hpb=46f19eadce5f3a11c0ae26934fd8d1b597906416;p=helm.git

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 4e0e04914..3c89150ad 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 )
 
@@ -189,7 +194,7 @@ let try_tactic ~tactic =
   mk_tactic (try_tactic ~tactic)
 ;;
 
-let fail = mk_tactic (fun _ -> raise (Fail "fail tactical"))
+let fail_tac = mk_tactic (fun _ -> raise (Fail "fail tactical"))
 
 (* This tries tactics until one of them doesn't _solve_ the goal *)
 (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
@@ -221,55 +226,3 @@ let solve_tactics ~tactics =
  in
   mk_tactic (solve_tactics ~tactics)
 ;;
-
-
-
-
-
-
-
-
-
-
-  (** tattica di prova per debuggare i tatticali *)
-(*
-let thens' ~start ~continuations status =
- let (proof,new_goals) = start status in
-  try
-   List.fold_left2
-    (fun (proof,goals) goal tactic ->
-      let (proof',new_goals') = tactic (proof,goal) in
-       (proof',goals@new_goals')
-    ) (proof,[]) new_goals continuations
-  with
-   Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
-
-let prova_tac =
- let apply_T_tac status =
-  let (proof, goal) = status in
-  let curi,metasenv,pbo,pty = proof in
-  let metano,context,gty = CicUtil.lookup_meta goal metasenv in
-   let rel =
-    let rec find n =
-     function
-        [] -> assert false
-      | (Some (Cic.Name name,_))::_ when name = "T" -> n
-      | _::tl -> find (n+1) tl
-    in
-     debug_print ("eseguo find");
-     find 1 context
-   in
-    debug_print ("eseguo apply");    
-    apply_tac ~term:(Cic.Rel rel) status
- in
-(*  do_tactic ~n:2 *)
-  repeat_tactic
-   ~tactic:
-    (then_
-      ~start:(intros_tac ~name:"pippo")
-      ~continuation:(thens' ~start:apply_T_tac ~continuations:[id_tac ; apply_tac ~term:(Cic.Rel 1)]))
-(* id_tac *)
-;;
-*)
-
-