- init_cache_and_tables rewritten using the automation_cache

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

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index d5ec8acfb8be6c9edee7f353ba9f5368f8314511..4a4f150b7bf3e27eb6d7beacdc50df2d84c4d82e 100644 (file)
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -201,6 +201,23 @@ let if_ ~start ~continuation ~fail =
    in
    PET.mk_tactic if_
 
+let ifs ~start ~continuations ~fail =
+   let ifs status =
+      let xoutput = 
+         try
+           let result = PET.apply_tactic start status in
+           info (lazy ("Tacticals.ifs: succedeed!!!"));
+           Some result 
+        with PET.Fail _ -> None
+      in
+      let tactic = match xoutput with
+         | Some res -> thens ~start:(const_tac res) ~continuations
+        | None     -> fail
+      in 
+      PET.apply_tactic tactic status
+   in
+   PET.mk_tactic ifs
+
 let first ~tactics =
   let rec first ~(tactics: tactic list) status =
     info (lazy "in Tacticals.first");
@@ -273,16 +290,18 @@ let solve_tactics ~tactics =
 
 let progress_tactic ~tactic =
   let msg = lazy "Failed to progress" in
-  let progress_tactic (((_,metasenv,_subst,_,_,_),_) as istatus) =
-    let ((_,metasenv',_subst,_,_,_),_) as ostatus =
+  let progress_tactic (((_,metasenv,_subst,_,_,_),g) as istatus) =
+    let ((_,metasenv',_subst,_,_,_),opened) as ostatus =
      PET.apply_tactic tactic istatus
     in
-     (*CSC: Warning
-       If just the index of some metas changes the tactic is recognized
-       as a progressing one. This is wrong. *)
-     if metasenv' = metasenv then
-      raise (PET.Fail msg)
-     else
-      ostatus
+    match opened with
+    | [g1] ->
+        let _,oc,oldty = CicUtil.lookup_meta g metasenv in
+        let _,nc,newty = CicUtil.lookup_meta g1 metasenv' in
+        if oldty = newty && oc = nc then
+          raise (PET.Fail msg)
+        else
+          ostatus
+    | _ -> ostatus
   in
   PET.mk_tactic progress_tactic