X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=1644186a1a558cca45538aa560b96387e9038e98;hb=dc7c02d8d8678d250a99dd6d012adcd69da63b75;hp=8887175b4d95a77cf969680b8ce6e9073be9d687;hpb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 8887175b4..1644186a1 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -93,12 +93,13 @@ let case_tac lab status =
     | [] -> assert false
     | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
       when is_fresh loc ->
-        let l_js = List.filter 
-                     (fun curloc -> 
-                        let _,_,metasenv,_,_ = status#obj in
-                        match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with
-                            Some s,_,_ when s = lab -> true
-                          | _ -> false) ([loc] @+ g') in
+        let l_js =
+          List.filter 
+           (fun curloc -> 
+              let _,_,metasenv,_,_ = status#obj in
+              match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with
+                  attrs,_,_ when List.mem (`Name lab) attrs -> true
+                | _ -> false) ([loc] @+ g') in
           ((l_js, t , [],`BranchTag)
            :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
     | _ -> fail (lazy "can't use relative positioning here")