From 0eabea8354445b2d81a92b9d1b3016a476d381cb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 1 Apr 2008 19:07:11 +0000 Subject: [PATCH] better check for progress --- helm/software/components/tactics/tacticals.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 -- 2.39.2