+;;
+
+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 ]
+;;