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=01a57f0c45fa2851722bfac93e9f4e8bc8afceb6;hpb=8b1a49bbee9eea86eb74c040defe701370ca5893;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 01a57f0c4..1644186a1 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -87,6 +87,26 @@ let pos_tac i_s status =
    status#set_stack gstatus
 ;;
 
+let case_tac lab status =
+  let gstatus = 
+    match status#stack with
+    | [] -> 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
+                  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")
+  in
+   status#set_stack gstatus
+;;
+
 let wildcard_tac status =
   let gstatus = 
     match status#stack with