let id_tac status = status ;;
let print_tac print_status message status =
- if print_status then pp_status status;
+ if print_status then pp_tac_status status;
prerr_endline message;
status
;;
| `RightToLeft -> "eq" ^ suffix
in
block_tac
- [ select_tac ~where ~job:(`Substexpand 1) true;
+ [ select_tac ~where ~job:(`Substexpand 2) true;
exact_tac
("",0,
Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
if name = "_" then clear_tac [name] else id_tac ]
;;
+let name_counter = ref 0;;
+let intros_tac ?names_ref names s =
+ let names_ref, prefix =
+ match names_ref with | None -> ref [], "__" | Some r -> r, "H"
+ in
+ if names = [] then
+ repeat_tac
+ (fun s ->
+ incr name_counter;
+ (* TODO: generate better names *)
+ let name = prefix ^ string_of_int !name_counter in
+ let s = intro_tac name s in
+ names_ref := !names_ref @ [name];
+ s)
+ s
+ else
+ block_tac (List.map intro_tac names) s
+;;
+
let cases ~what status goal =
let gty = get_goalty status goal in
let status, what = disambiguate status (ctx_of gty) what None in
) status
;;
+let inversion_tac ~what:(txt,len,what) ~where =
+ let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
+ let indtyinfo = ref None in
+ let sort = ref (NCic.Rel 1) in
+ atomic_tac (block_tac [
+ analyze_indty_tac ~what indtyinfo;
+ (fun s -> select_tac
+ ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
+ sort_of_goal_tac sort;
+ (fun status ->
+ let ity = HExtlib.unopt !indtyinfo in
+ let NReference.Ref (uri, _) = ity.reference in
+ let name =
+ NUri.name_of_uri uri ^ "_inv_" ^
+ snd (NCicElim.ast_of_sort
+ (match !sort with NCic.Sort x -> x | _ -> assert false))
+ in
+ let eliminator =
+ let _,_,w = what in
+ Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+ in
+ exact_tac ("",0,eliminator) status) ])
+;;