X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Ftacticals.ml;h=4a4f150b7bf3e27eb6d7beacdc50df2d84c4d82e;hb=d990d5c64d0b9c07baef4257e7931321a42ae695;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..4a4f150b7 100644
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -296,9 +296,9 @@ let progress_tactic ~tactic =
     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