Much ado about nothing:

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

diff --git a/components/tactics/tacticals.ml b/components/tactics/tacticals.ml
index 63b8e12b59a362ddafa4deb855bf215ecf6db5be..3e9c1db2cbb59f2db82f313b5b934f6058ea8657 100644 (file)
--- a/components/tactics/tacticals.ml
+++ b/components/tactics/tacticals.ml
@@ -183,15 +183,14 @@ let seq ~tactics =
 (* Tacticals that cannot be implemented on top of tynycals *)
 
 let first ~tactics =
-  let rec first ~(tactics: (string * tactic) list) status =
+  let rec first ~(tactics: tactic list) status =
     info (lazy "in Tacticals.first");
     match tactics with
       [] -> raise (PET.Fail (lazy "first: no tactics left"))
-    | (descr, tac)::tactics ->
-        info (lazy ("Tacticals.first IS TRYING " ^ descr));
+    | tac::tactics ->
         try
          let res = PET.apply_tactic tac status in
-          info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
+          info (lazy ("Tacticals.first: succedeed!!!"));
           res
         with 
          PET.Fail _ -> first ~tactics status
@@ -230,18 +229,16 @@ let rec repeat_tactic ~tactic =
 
 (* This tries tactics until one of them solves the goal *)
 let solve_tactics ~tactics =
- let rec solve_tactics ~(tactics: (string * tactic) list) status =
+ let rec solve_tactics ~(tactics: tactic list) status =
   info (lazy "in Tacticals.solve_tactics");
   match tactics with
-  | (descr, currenttactic)::moretactics ->
-      info (lazy ("Tacticals.solve_tactics is trying " ^ descr));
+  | currenttactic::moretactics ->
       (try
         let (proof, opened) as output_status =
          PET.apply_tactic currenttactic status 
         in
         match opened with 
-          | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^ 
-                   " solved the goal!!!"));
+          | [] -> info (lazy ("Tacticals.solve_tactics: solved the goal!!!"));
                   output_status
           | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
                  raise (PET.Fail (lazy "Goal not solved"))