]
;;
-let apply_tac (s,n,t) = exact_tac (s,n,Ast.Appl [t; Ast.Implicit `Vector]);;
+let apply_tac (s,n,t) =
+ let t = Ast.Appl [t; Ast.Implicit `Vector] in
+ exact_tac (s,n,t)
+;;
type indtyinfo = {
rightno: int;
let compute_goal_sort_tac = distribute_tac (fun status goal ->
let goalty = get_goalty status goal in
let status, goalsort = typeof status (ctx_of goalty) goalty in
+ let goalsort = fix_sorts goalsort in
sort := Some goalsort;
exec id_tac status goal)
in
| _ -> assert false
in
let name =
- match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq" ^ suffix
+ match dir with
+ `LeftToRight -> "eq" ^ suffix ^ "_r"
+ | `RightToLeft -> "eq" ^ suffix
in
block_tac
[ select_tac ~where ~job:(`Substexpand 1) true;
if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
;;
+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);;
+
let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
let gty = get_goalty status goal in
let eq status ctx t1 t2 =