X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=87be3279f18ade3f1f49ad8bbebb443e94251d9c;hb=5fa31e43ffe25aa7b1539653b137968b5cf9899a;hp=40a490d6bb5941bf736edbd61532e769f49acf7e;hpb=d072c3ea699cf33189d18d8431fda9750fc2eb93;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 40a490d6b..87be3279f 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -288,6 +288,14 @@ let typeof status where t =
   None, ctx, ty
 ;;
   
+let whd status ?delta where t =
+  let _,_,metasenv,subst,_ = status.pstatus in
+  let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
+  let _,_,t = relocate ctx t in
+  let t = NCicReduction.whd ~subst ?delta ctx t in
+  None, ctx, t
+;;
+  
 let unify status where a b =
   let n,h,metasenv,subst,o = status.pstatus in
   let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
@@ -521,4 +529,28 @@ let intro_tac name =
  exact_tac
   ("",0,(CicNotationPt.Binder (`Lambda,
    (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)))
-;; 
+;;
+
+let case status goal =
+ let _,ctx,_ = get_goal status goal in
+ let ty = typeof status (`Ctx ctx) ("",ctx,NCic.Rel 1) in
+ let ref =
+  match whd status (`Ctx ctx) ty with
+     _,_,NCic.Const ref
+   | _,_,NCic.Appl (NCic.Const ref :: _) -> ref
+   | _,_,_ -> fail (lazy ("not an inductive type")) in
+ let _,_,tl,_,i = NCicEnvironment.get_checked_indtys ref in
+ let _,_,_,cl = List.nth tl i in
+ let consno = List.length cl in
+ let t =
+  NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1,HExtlib.mk_list (NCic.Implicit `Term) consno)
+ in
+ let status,t,ty = refine status (`Ctx ctx) ("",ctx,t) None in
+ instantiate status goal t
+;;
+
+let case_tac = distribute_tac case;;
+
+let case1_tac name =
+ block_tac [ intro_tac name; case_tac ]
+;;