X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Ftacticals.ml;h=34ecb2d99d1c68f6f18a58cca383cb396358f663;hb=95adf6dc8e29a71adc34e71eafe3f427990126e0;hp=6e91de1fcd4194e02322dcce88598dd63cbe1370;hpb=ee61e81b4b780abb311973a8b907ba56d5011d0b;p=helm.git

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index 6e91de1fc..34ecb2d99 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, _subst, _, _, _ = proof in
+  let _, metasenv, _, _, _, _ = 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, _subst, _ , _, _ = proof in
+  let _, metasenv, _, _ , _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
    raise (PET.Fail (lazy "fail tactical"))
  in
@@ -290,15 +290,15 @@ let solve_tactics ~tactics =
 
 let progress_tactic ~tactic =
   let msg = lazy "Failed to progress" in
-  let progress_tactic (((_,metasenv,_subst,_,_,_),g) as istatus) =
-    let ((_,metasenv',_subst,_,_,_),opened) as ostatus =
+  let progress_tactic (((_,metasenv,_,_,_,_),g) as istatus) =
+    let ((_,metasenv',_,_,_,_),opened) as ostatus =
      PET.apply_tactic tactic istatus
     in
     match opened with
     | [g1] ->
-        let _,_,oldty = CicUtil.lookup_meta g metasenv in
-        let _,_,newty = CicUtil.lookup_meta g1 metasenv' in
-        if oldty = newty then
+        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