From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 1 Apr 2008 14:08:11 +0000 (+0000)
Subject: progress made better, still not perfect
X-Git-Tag: make_still_working~5478
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ee61e81b4b780abb311973a8b907ba56d5011d0b;p=helm.git

progress made better, still not perfect
---

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index f647ebcca..6e91de1fc 100644
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -290,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 _,_,oldty = CicUtil.lookup_meta g metasenv in
+        let _,_,newty = CicUtil.lookup_meta g1 metasenv' in
+        if oldty = newty then
+          raise (PET.Fail msg)
+        else
+          ostatus
+    | _ -> ostatus
   in
   PET.mk_tactic progress_tactic