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