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

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 01a57f0c4..8887175b4 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -87,6 +87,25 @@ 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
+                            Some s,_,_ when s = lab -> 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