+let case ~what status goal =
+ let gty = get_goalty status goal in
+ let status, what = disambiguate status what None (ctx_of gty) in
+ let ty = typeof status (ctx_of what) what in
+ let ref, consno, left, right = analyse_indty status ty in
+ let t =
+ NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1,
+ HExtlib.mk_list (NCic.Implicit `Term) consno)
+ in
+ let ctx = ctx_of gty in
+ let status,t,ty = refine status ctx (mk_cic_term ctx t) None in
+ instantiate status goal t
+;;
+
+let case_tac ~what = distribute_tac (case ~what);;
+
+let case1_tac name =
+ block_tac [ intro_tac name;
+ case_tac ~what:("",0,CicNotationPt.Ident (name,None)) ]
+;;