...

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 8887175b4d95a77cf969680b8ce6e9073be9d687..1644186a1a558cca45538aa560b96387e9038e98 100644 (file)
--- 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")