+let constructor ?(num=1) ~args status goal =
+ if num < 1 then fail (lazy "constructor numbers begin with 1");
+ let gty = get_goalty status goal in
+ let status, (r,_,_,_) = analyse_indty status gty in
+ let ref = NReference.mk_constructor num r in
+ let t =
+ if args = [] then Ast.NRef ref else
+ Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector]
+ ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args))
+ in
+ exec (apply_tac ("",0,t)) status goal
+;;
+
+let constructor_tac ?num ~args = distribute_tac (constructor ?num ~args);;
+