X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Ftacticals.ml;h=f3f7793032365bb5194137002b9356e0a2a80881;hb=513a2c58442fcfb2545bbc2b146d5a73051d6740;hp=eb3ebc1bba506c4a748b846d36a45a968fe814ec;hpb=4989069e8c6910461913fc9a2bae104a0e0259b2;p=helm.git

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index eb3ebc1bb..f3f779303 100644
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -42,7 +42,7 @@ module PET = ProofEngineTypes
 
 let id_tac = 
  let id_tac (proof,goal) = 
-  let _, metasenv, _, _, _ = proof in
+  let _, metasenv, _subst, _, _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
   (proof,[goal])
  in 
@@ -50,7 +50,7 @@ let id_tac =
 
 let fail_tac =
  let fail_tac (proof,goal) =
-  let _, metasenv, _, _, _ = proof in
+  let _, metasenv, _subst, _ , _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
    raise (PET.Fail (lazy "fail tactical"))
  in
@@ -108,8 +108,6 @@ struct
 
   type tactic = PET.tactic
 
-  let id_tactic = id_tac
-
   (* f is an eval function of a machine;
      the machine is applied to a fresh stack and the final stack is read
      back to obtain the result of the tactic *)
@@ -130,12 +128,7 @@ struct
     let opened_goals, closed_goals = goals_diff ~before ~after ~opened in
     (proof', opened_goals, closed_goals), stack
 
-  let get_status (status, _) = status
-  let get_proof ((proof, _, _), _) = proof
-
   let goals ((_, opened, closed), _) = opened, closed
-  let set_goals (opened, closed) ((proof, _, _), stack) =
-    (proof, opened, closed), stack
 
   (* Done only at the beginning of the eval of the machine *)
   let get_stack = snd
@@ -190,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
@@ -237,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"))
@@ -265,8 +255,8 @@ let solve_tactics ~tactics =
 
 let progress_tactic ~tactic =
   let msg = lazy "Failed to progress" in
-  let progress_tactic (((_,metasenv,_,_,_),_) as istatus) =
-    let ((_,metasenv',_,_,_),_) as ostatus =
+  let progress_tactic (((_,metasenv,_subst,_,_,_),_) as istatus) =
+    let ((_,metasenv',_subst,_,_,_),_) as ostatus =
      PET.apply_tactic tactic istatus
     in
      (*CSC: Warning