From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 1 Apr 2008 19:07:11 +0000 (+0000)
Subject: better check for progress
X-Git-Tag: make_still_working~5475
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0eabea8354445b2d81a92b9d1b3016a476d381cb;p=helm.git

better check for progress
---

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