REMARK_TAC : string -> tactic

SYNOPSIS: A tactic version of remark.
DESCRIPTION: Given any goal A ?- p, the tactic REMARK_TAC s prints the string s to standard output. As remark does, this outputs a string only if verbose flag is set.
FAILURE CONDITIONS: Never fails.
SEE ALSO: PRINT_GOAL_TAC, remark, verbose